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
 softtyping 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(01)  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**521, 2**10+1 .. 2**101)).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 !< 01) ; x 
  with f01 !! 01 > 01 
In the following, we assume:
not := True > False ;; False > True
# which implies not !! Bool > Bool
inv := 0 > 1 ;; 1 > 0
# which implies inv !! 01 > 01
i !< 01
b !< Bool
overloading ad'hoc
not(b)  !!  Bool 
inv(i)  !!  01 
inv(b)  illegal  Bool not compatible with 01 
not(i)  illegal  01 not compatible with Bool 
(not & inv)(b)  !!  Bool 
(not & inv)(i)  !!  01 
(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(01)) ; 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) 
polymorphic update (example from chapter 32 of Types and Programming Languages)
from Book  in merd (non sugared!) 
s = {x={a=5,b=6},y=true}  s = X(A(5)&B(6)) & Y(True) 
s < x={a=8}  s.(X(_) & r > X(A(8)) & r) 
f = lambda X<:{#a:Nat}. lambda r:X. r < a = succ(r.a)  f := A(n) & r > A(n+1) & r 
f : forall X<:{#a:Nat}. X < X  f !! x > (x !< A(Addable)) ; x 
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 compiletime (they still are first class values)
 they are not manipulated directly, but using a little sugar
 together with Open_function, they can achieve mixins (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 upperbound 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 > 101
::< := 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) ; 101)
::< := Open_function(o,o > (o !< Ordered) ; Bool)
You can define:
a == b := a<=>b == 0
(invariance is also called novariance)
Problem
are List(Int)  List(String) and List(Int  String) the same ?
Answer
no!
 [ 1, "foo" ] is not a List(Int)  List(String)
 [ 1, "foo" ] is a List(Int  String)
Question
in which case does c(a)  c(b) = c(ab) holds?
Examples
 Maybe
Maybe(a) = None  Some(a)
aka Maybe = (_ > None)  Some
Maybe(a)  Maybe(b)
= (None  Some(a))  (None  Some(b))
= None  Some(a)  None  Some(b)
= None  Some(a)  Some(b)
= None  Some(ab)
= Maybe(ab)
 AB
AB(a) = A(a)  B(a)
aka AB = A  B
AB(a)  AB(b)
= (A(a)  B(a))  (A(b)  B(b))
= A(a)  A(b)  B(a)  B(b)
= A(ab)  B(ab)
= AB(ab)
 AA
AA(a) = A(a,a)
AA(a)  AA(b)
= A(a,a)  A(b,b)
= A( (a,a)  (b,b) )
<> A(ab, ab)
since (a,a)  (b,b) !< (ab,ab)
but (a,a)  (b,b) !> (ab,ab) is false
eg: (12, 12) is (1, 1)  (1, 2)  (2, 1)  (2, 2)
!> (1, 1)  (2, 2)
 List
List(a) = Nil  Cons(a, List(a))
List(a)  List(b)
= (Nil  Const(a, List(a)))  (Nil  Const(b, List(b)))
= Nil  Const(a, List(a))  Nil  Const(b, List(b))
= Nil  Const(a, List(a))  Const(b, List(b))
= Nil  Const( (a, List(a))  (b, List(b)) )
<> Nil  Const(ab, List(ab))
Conclusion
So in which case c(a)  c(b) => c(ab) ??
Well: if c(a) = e1  e2  ...  en where each "ei" use at most one "a"
 it works for "Maybe" ("Some" uses ony one "a", "None" uses none)
 it works for "AB" (both "A" and "B" use only one "a")
 it fails for "AA" and "List"
Terminology
I don't know what's the terminology for this propriety:
when we have  "c" is 
c(a)  c(b) !< c(ab)  covariant 
c(a)  c(b) !> c(ab)  contravariant 
c(a)  c(b) !! c(ab)  ? distributive 
More: if c(a)  c(b) => c(ab)
we also have c(a) & c(b) => c(a&b)
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 nonmutable data.
Out
"Inout" doesn't make the difference between readwrite and writeonly types.
"out" is contravariant: out(t1) < out(t2) if t1 > t2
References
 Introduction to types
 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.12 2003/01/09 18:30:56 pixel_ Exp $