This gives many examples of the types in merd.
You can find some explainations of the type system here.
On the theory side:
- intersection types
- union types
- bounded quantification
- soft-typing like type inference
- no conditional constraints
- no flow analysis (but uses fresh types per each pattern in pattern matching matches)
Very brief syntax explaination
See detailed information on syntax for more.
operators
0 | 1 | union of 0 and 1 |
0 |&| False | intersection of 0 and False |
foo !! bar | foo has type bar |
foo !> bar | foo's type is a subtype of bar |
foo !> bar | foo's type is a supertype of bar |
x -> x | identity function |
x,y -> y,x | swap function |
False -> True ;; True -> False | function using pattern matching (boolean "not") |
Types of simple expressions
This diagram shows the various values and the relation between them.
(jpg,pdf)
first order
0 | !! | 0 |
0 |&| 1 | !! | 0 |&| 1 |
0, 1 | !! | 0, 1 |
[ 0, 1 ] | !! | List(0 | 1) |
[ 0, True ] | !! | List(0 | True) |
simple functions
0 -> 0 | !! | 0 -> 0 |
x -> x | !! | x -> x |
x -> x,x | !! | x -> x,x |
x,y -> y,x | !! | x,y -> y,x |
functions using pattern matching
0 -> 0 ;; 1 -> 1 | !! | 0 | 1 -> 0 | 1 |
0 -> 0 ;; 1 -> 0 | !! | 0 | 1 -> 0 |
0 -> 0 ;; 0 -> 1 | !! | 0 -> 0 | 1 |
True -> False ;; False -> True | !! | True | False -> True | False |
None -> None ;; Some(x) -> Some(x) | !! | None | Some(x) -> None | Some(x) |
Naming types
If you name a type, the name is used to simplify the types displayed:
Bool = True | False
Maybe(x) = None | Some(x)
True -> False ;; False -> True | !! | Bool -> Bool |
None -> None ;; Some(x) -> Some(x) | !! | Maybe(x) -> Maybe(x) |
Note that this is not a type declaration, but it is used to restrict the use of constructors:
- [ Leaf(1), Leaf(True) ] is a valid expression
- but it isn't valid anymore if a type Tree = Leaf(0|1) | Node(Tree, Tree) has been declared.
- it is valid again if another type TreeB = Leaf(True) | Node(TreeB, TreeB) has been declared.
=> a constructor used in a type is no more fully polymorphic. The goal is to catch more errors.
Some other common types:
Byte = Builtin::Or_range(0, 255)
Uint = Builtin::Or_range(0, 2147483647) # 2**31 - 1
Int = Builtin::Or_range(-2147483648, 2147483647)
Char = Builtin::Or_range("\x00", "\xff") # 8bit chars, to be extended with Unicode
# Float *could* be described as follow:
# Float = (list_product(-2**52 .. 2**52-1, -2**10+1 .. 2**10-1)).map(mant,exp -> mant / 2**51 * 2**exp).range
Note the structural subtyping:
- Char < String (where String is the infinite union of strings)
- Byte < Uint < Int
- Int < Integer < Rational (where Integer is math Z, Rational is math Q)
- Int < Float < Rational (note that Float really are C's double, and do include 32 bits integers)
Type constraints
function call
(0 -> 0)(i) | implies | i !< 0 |
if b then 0 else 1 | implies | b !< Bool |
assignment
i = 0 | implies | i !> 0 |
j = i | implies | j !> i |
i = 0 ; i = 1 | implies | i !> 0 | 1 |
i = if b then 0 else 1 | implies | b !< Bool ; i !> 0 | 1 |
i = if b then y else z | implies | b !< Bool ; i !> y | z |
bounded polymorphism
0 -> 1 ;; x -> 2 | !! | x -> (x !> 0) ; 1 | 2 |
0 -> 1 ;; x -> x | !! | x -> (x !> 0 | 1) ; x |
| | (could also be x -> (x !> 0) ; x | 1 which is the same) |
x -> (0 -> 1)(x), x | !! | x -> (x !< 0) ; 1, x |
0 -> 1 ;; x -> f01(x) | !! | x -> (x !> 0) ; (x !< 0|1) ; x |
| | with f01 !! 0|1 -> 0|1 |
In the following, we assume:
not := True -> False ;; False -> True
# which implies not !! Bool -> Bool
inv := 0 -> 1 ;; 1 -> 0
# which implies inv !! 0|1 -> 0|1
i !< 0|1
b !< Bool
overloading ad'hoc
not(b) | !! | Bool |
inv(i) | !! | 0|1 |
inv(b) | illegal | Bool not compatible with 0|1 |
not(i) | illegal | 0|1 not compatible with Bool |
(not |&| inv)(b) | !! | Bool |
(not |&| inv)(i) | !! | 0|1 |
(not |&| inv)(x) | illegal? | choice must be done at compile time ? |
Note the similarity between 0 -> 1 ;; 1 -> 0 (pattern matching) and (0 -> 1) |&| (1 -> 0) (overloading)
which are both valid expressions, but which don't have the same types.
records
X(0) | !! | X(0) |
X(0) |&| Y(1) | !! | X(0) |&| Y(1) |
  |
get0 := X(0) -> () | implies | get0 !! X(0) -> () |
get1 := X(0) -> () ;; x -> () | implies | get1 !! x -> (x !> 0) ; () |
get0(X(0)), get0(Y(1)), get0(X(1) |&| Y(1)) | is | (), illegal, () |
get1(X(0)), get1(Y(1)), get1(X(1) |&| Y(1)) | is | (), (), () |
  |
inc0 := X(0) -> X(1) | implies | inc0 !! X(0) -> X(1) |
inc1 := (X(0) |&| x) -> (X(1) |&| x) | implies | inc1 !! (X(0) |&| x) -> (X(1) |&| x) |
inc2 := X(0) -> X(1) ;; x -> x | implies | inc2 !! x -> (x !> X(0|1)) ; x |
inc0(X(0)), inc0(Y(1)), inc0(X(0) |&| Y(1)) | is | X(1), illegal, X(1) |
inc1(X(0)), inc1(Y(1)), inc1(X(0) |&| Y(1)) | is | X(1), illegal, X(1) |&| Y(1) |
inc2(X(0)), inc2(Y(1)), inc2(X(0) |&| Y(1)) | is | X(1), Y(1), X(1) |&| Y(1) |
0 |&| True is a valid value which can be used both as 0 and True.
It needs investigating the advantage of this. Here are some examples:
- 1|&|"foo" + 1|&|"bar" gives 2|&|"foobar"
- [ 1, "foo" ].map(x -> x + 1|&|"bar") gives [ 2, "foobar" ]
- 0 |&| "" |&| [] as a default value to initialize variables
- (min, sec) = s.m("(\d+):(\d+)") is a regexp returning type Int|&|String, Int|&|String.
This enables:
- min * 60 + sec where min and sec are used as numbers
- print_string(min)
abstract types
Intersection of abstract types is very interesting, see below.
Abstract types
Abstract types are atomic types:
- being types, they can only be manipulated at compile-time (they still are first class values)
- they are not manipulated directly, but using a little sugar
- together with Open_function, they can achieve mix-ins (aka type classes)
- implementation subtyping is used (thick arrows on the diagram)
Simple example
Addable = class
::+ := o,o -> o
# removed += times to simplify
is sugar for
Addable = &Addable
::+ := Open_function(o,o -> (o !< Addable) ; o)
The Open_function construct enables virtual functions. This is the "open world" overloading.
At a given time, the compiler must go in the "closed world". It looks for types implementing the "+" function.
We typically have Byte, Uint, Int, Integer, Real, Rational, String, List.
-
x -> x + 1 !! x -> (x !> 1) ; (x !< Addable) ; x
# when going closed world:
!! x -> (x !> 1) ; (x !< Rational) ; x
Rational is chosen here as the upper-bound of the various types
verifying lower bounded by 1 and upper bounded by Addable. Strings
and lists are discarded.
-
x -> x + 1|&|"foo" !! x -> (x !> 1|&|"foo") ; (x !< Addable) ; x
# when going closed world:
!! x -> (x !> 1|&|"foo") ; (x !< Rational | String) ; x
The "when to go closed world" is still to be defined :)
Interface inheritance
Eq = class
::== := o,o -> Bool
::!= := o,o -> Bool
Ordered = Eq |&| class
::<=> := o,o -> -1|0|1
::< := o,o -> Bool
# removed <= > >= min max to simplify
is sugar for
Eq = &Eq
::== := Open_function(o,o -> (o !< Eq) ; Bool)
::!= := Open_function(o,o -> (o !< Eq) ; Bool)
Ordered = Eq |&| &Ordered
::<=> := Open_function(o,o -> (o !< Ordered) ; -1|0|1)
::< := Open_function(o,o -> (o !< Ordered) ; Bool)
You can define:
a == b := a<=>b == 0
Mutability
Inout
mutable types are invariant:
t1 !< Inout(t2) implies t1 !! t2
t1 !> Inout(t2) implies t1 !! t2
- beware of common place errors:
- record subtyping (aka data inheritance)
Inout(X(Int) /\ Y(Int)) < Inout(X(Int)) is *false*
but
X(Inout(Int)) /\ Y(Inout(Int)) < X(Inout(Int)) is true!
so no need for a special ugly rule for data inheritance.
- containers subtyping
Inout(List(car)) < Inout(List(vehicle)) is *false*
List(Inout(car)) < List(Inout(vehicle)) is *false*
but
List(car) < List(vehicle) is true!
List(X(Inout(Int)) /\ Y(Inout(Int))) < List(X(Inout(Int))) is true!
(since List(X(Inout(Int)) /\ Y(Inout(Int))) = List(X(Inout(Int))) /\
List(Y(Inout(Int))))
OO languages have a hard time with this since they usually do not make the
difference between mutable and non-mutable data.
Out
"Inout" doesn't make the difference between read-write and write-only types.
"out" is contravariant: out(t1) < out(t2) if t1 > t2
References
- Union and intersection types
- Bounded polymorphism
- Intersection values
- Precise types
Pixel
This document is licensed under GFDL (GNU Free Documentation License).
Release: $Id: types.html,v 1.8 2002/05/17 15:22:57 pixel_ Exp $