Difference between revisions of "SCL Types"
(4 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
+ | [[Category: Simantics Constraint Language]] | ||
== Basic types == | == Basic types == | ||
Line 76: | Line 77: | ||
SCL functions are [http://en.wikipedia.org/wiki/Referential_transparency_(computer_science) referentially transparent] which means that they are like mathematical functions always returning the same value for the same parameters and not causing any observable side-effects. This seems extremely restrictive because most of the programs are written in order to generate some kind of side-effects and even completely mathematical algorithms involve functions that are not referentially transparent such as generation of random numbers. | SCL functions are [http://en.wikipedia.org/wiki/Referential_transparency_(computer_science) referentially transparent] which means that they are like mathematical functions always returning the same value for the same parameters and not causing any observable side-effects. This seems extremely restrictive because most of the programs are written in order to generate some kind of side-effects and even completely mathematical algorithms involve functions that are not referentially transparent such as generation of random numbers. | ||
− | This policy does not however restrict expressive power of the language because functions can return and manipulate ''descriptions of computations''. These computations are then executed some external means. Two different ways of handling computations in SCL are monads and effect types. The former concept is described [http://www.haskell.org/haskellwiki/Monad_tutorials_timeline (in)numerable] times in different Haskell tutorials, for example [http://ertes.de/articles/monads.html], and is defined with the machinery already described. | + | This policy does not however restrict expressive power of the language because functions can return and manipulate ''descriptions of computations''. These computations are then executed by some external means. Two different ways of handling computations in SCL are monads and effect types. The former concept is described [http://www.haskell.org/haskellwiki/Monad_tutorials_timeline (in)numerable] times in different Haskell tutorials, for example [http://ertes.de/articles/monads.html], and is defined with the machinery already described. Effect types are not applicable to as large range of different computation concepts as monads are but they are easier to work with. |
− | + | An effectful computation has type <effects> value. The type after angle brackets is the type of the value obtained by the computation. Side-effects that might happen during computation are listed inside of angle brackets. Effect types must always occur as a return type of a function. Here are some examples of functions with side-effects: | |
<pre> | <pre> | ||
− | randomBetween : Double -> Double -> <Nondet> Double | + | randomBetween :: Double -> Double -> <Nondet> Double |
− | resourceByUri : String -> <ReadGraph> Resource | + | resourceByUri :: String -> <ReadGraph> Resource |
− | claim : Resource -> Resource -> Resource -> <WriteGraph> () | + | claim :: Resource -> Resource -> Resource -> <WriteGraph> () |
− | randomLiteral : Double -> Double -> <Nondet,WriteGraph> Resource | + | randomLiteral :: Double -> Double -> <Nondet,WriteGraph> Resource |
+ | </pre> | ||
+ | |||
+ | Effect types are much like type constraints: you can mostly ignore them when using functions. All effects you use are automatically collected and added to the type signature of the defined function (or checked against type annotation if provided). | ||
+ | |||
+ | Like type classes, effects form a hierarchy. For example WriteGraph inherits ReadGraph and a function both reading and writing to graph is annotated only with <WriteGraph> effect. | ||
+ | |||
+ | Like types, effects can also be abstracted with effect variables. This is important when defining generic functions that manipulate possibly effectful functions: | ||
+ | <pre> | ||
+ | executeTwice :: (() -> <e> ()) -> <e> () | ||
+ | executeTwice f = do f () ; f () | ||
+ | |||
+ | (.) :: (b -> <e2> c) -> (a -> <e1> b) -> (a -> <e1,e2> c) | ||
+ | (f . g) x = f (g x) | ||
</pre> | </pre> |
Latest revision as of 13:50, 27 June 2013
Basic types
SCL is statically typed language which means that types of the possible values of all variables are known already at compile time. The following types (or more exactly, type constructors) have builtin support:
- Boolean
- Byte, Short, Integer, Long
- Float, Double
- String
- BooleanArray, ByteArray, ShortArray, IntegerArray, LongArray, FloatArray, DoubleArray
- []
- (), (,), (,,), ...
- (->)
- Maybe
- Array
Other type constructors are either imported from the host language or defined in SCL modules. Except for the couple of special cases in the previous list, the names of all type constructors are capitalized.
Some type constructors are parametric (compare to generics in Java or templates in C++). For example, the list type constructor [] has one parameter: the type of the list elements. Thus [Integer] is the type of the integer lists and [String] is the type of string lists. [[Integer]] is the type of the lists of integer lists. Parameters are usually written after the parametric type constructor: for example Maybe String or Array Integer, but some of the builtin type constructors can be written in a special way in order to make the type expressions more readable:
[a] = [] a (a,b) = (,) a b (a,b,c) = (,,) a b c ... a -> b = (->) a b
Particularly important type constructor is (->) for building function types. For example, the type of the function computing the length of a string is String -> Integer: the function takes a string as a parameter and returns an integer.
Types of the functions taking multiple parameters are written by composing function types. For example, the type of a function taking nth element of a string list is [String] -> Integer -> String. The function takes a string list and an integer as a parameter and returns a string. Function type operator -> is right associative thus the previous type is equivalent to [String] -> (Integer -> String). Thus the type expression can be read as well as a type of functions taking a string list and returning another function from integers and strings.
(a,b) is the type of pairs where the first component of the pair has type a and the second component has type b. Tuple types (a,b,c), (a,b,c,d) etc. are defined similarly. Maybe a is the type of optional values.
Type variables
Many functions can be defined so that they do not need to know the exact types they are operating with. Such unknown types can be filled in type expressions by type variables: for example the function we discussed earlier that took nth element of a string list does not need the information that list elements are strings in its implementation and so it can be given a more generic type [a] -> Integer -> a, i.e a function taking a list of a:s and an integer as a parameter and returning a single a.
Function types with type variables tell quite much about the function assuming it is total, i.e does not hang or throw a runtime exception with any parameters. For example the type signatures define the following functions uniquely:
id :: a -> a swap :: (a,b) -> (b,a) const :: a -> b -> a
and there are only two possible total functions satisfying the following signature
choose :: a -> a -> a
Type variables may also refer to parametric types, but all useful examples involve type constraints we describe below.
Type constraints
SCL does not support function overloading at least in the way Java and C++ support it. This means that every function has a unique type signature. Now consider the addition function (+). We could defined its signature for example as Integer -> Integer -> Integer, but then we would need some other name for the sum of doubles Double -> Double -> Double or strings String -> String -> String. It would seem like the right signature would be a -> a -> a, but that is not satisfactory either, because then the function had to somehow support all possible types.
The solution to the problem is to constraint the set of allowed types for the type variable. Such a constrained type is written in the case of addition function as Additive a => a -> a -> a. The constraint Additive a is composed of a type class Additive followed by parameters of the constraint. The type can be understood in two different ways. A logical reading is
for any additive type a, the function takes two a:s as parameters and returns a
and operational reading that gives a good intuition what is happening in runtime
the function takes a parameter Additive a that describes a set of methods that can be used to operate values of a and two a:s and returns a
Constrained type variable can be also parametric. For example, let's say we want to define a function getNth that takes nth element of a list but also works with arrays. The signature would then be
getNth :: Sequence s => s a -> Integer -> a
Type classes form a hierarchy: each class may have any number of superclasses. Only the most specific type class is needed in the constraints. For example, addition and multiplication have the following signatures:
(+) :: Additive a => a -> a -> a (*) :: Ring a => a -> a -> a
and Additive is a superclass of Ring a. A function using both operators need to specify only Ring as a constraint:
doubleAndAddOne :: Ring a => a -> a doubleAndAddOne x = 2*x + 1
Effect types
SCL functions are referentially transparent which means that they are like mathematical functions always returning the same value for the same parameters and not causing any observable side-effects. This seems extremely restrictive because most of the programs are written in order to generate some kind of side-effects and even completely mathematical algorithms involve functions that are not referentially transparent such as generation of random numbers.
This policy does not however restrict expressive power of the language because functions can return and manipulate descriptions of computations. These computations are then executed by some external means. Two different ways of handling computations in SCL are monads and effect types. The former concept is described (in)numerable times in different Haskell tutorials, for example [1], and is defined with the machinery already described. Effect types are not applicable to as large range of different computation concepts as monads are but they are easier to work with.
An effectful computation has type <effects> value. The type after angle brackets is the type of the value obtained by the computation. Side-effects that might happen during computation are listed inside of angle brackets. Effect types must always occur as a return type of a function. Here are some examples of functions with side-effects:
randomBetween :: Double -> Double -> <Nondet> Double resourceByUri :: String -> <ReadGraph> Resource claim :: Resource -> Resource -> Resource -> <WriteGraph> () randomLiteral :: Double -> Double -> <Nondet,WriteGraph> Resource
Effect types are much like type constraints: you can mostly ignore them when using functions. All effects you use are automatically collected and added to the type signature of the defined function (or checked against type annotation if provided).
Like type classes, effects form a hierarchy. For example WriteGraph inherits ReadGraph and a function both reading and writing to graph is annotated only with <WriteGraph> effect.
Like types, effects can also be abstracted with effect variables. This is important when defining generic functions that manipulate possibly effectful functions:
executeTwice :: (() -> <e> ()) -> <e> () executeTwice f = do f () ; f () (.) :: (b -> <e2> c) -> (a -> <e1> b) -> (a -> <e1,e2> c) (f . g) x = f (g x)