This gives many examples of the types in merd. You can find some explainations of the type system here.

On the theory side:


Very brief syntax explaination

See detailed information on syntax for more.

operators

0 | 1union of 0 and 1
0 |&| Falseintersection of 0 and False
foo !! barfoo has type bar
foo !< barfoo's type is a subtype of bar
foo !> barfoo's type is a supertype of bar
x -> xidentity function
x,y -> y,xswap function
False -> True ;; True -> Falsefunction 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: => 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:

Type constraints

function call

(0 -> 0)(i)impliesi !< 0
if b then 0 else 1impliesb !< Bool

assignment

i = 0impliesi !> 0
j = iimpliesj !> i
i = 0 ; i = 1impliesi !> 0 | 1
i = if b then 0 else 1impliesb !< Bool ; i !> 0 | 1
i = if b then y else zimpliesb !< 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

Intersection values

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)illegalBool not compatible with 0|1
not(i)illegal0|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) -> ()impliesget0 !! X(0) -> ()
get1 := X(0) -> () ;; x -> ()impliesget1 !! 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)impliesinc0 !! X(0) -> X(1)
inc1 := (X(0) |&| x) -> (X(1) |&| x)impliesinc1 !! (X(0) |&| x) -> (X(1) |&| x)
inc2 := X(0) -> X(1) ;; x -> ximpliesinc2 !! x -> (x !> X(0|1)) ; x
inc0(X(0)), inc0(Y(1)), inc0(X(0) |&| Y(1))isX(1), illegal, X(1)
inc1(X(0)), inc1(Y(1)), inc1(X(0) |&| Y(1))isX(1), illegal, X(1) |&| Y(1)
inc2(X(0)), inc2(Y(1)), inc2(X(0) |&| Y(1))isX(1), Y(1), X(1) |&| Y(1)
polymorphic update (example from chapter 32 of Types and Programming Languages)
from Bookin 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

free intersection values

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:

abstract types

Intersection of abstract types is very interesting, see below.

Abstract types

Abstract types are atomic types:

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. 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

Covariance, invariance

(invariance is also called novariance)

Covariance and Contravariance, Distributivity?

Problem

are List(Int) | List(String) and List(Int | String) the same ?

Answer

no!

Question

in which case does c(a) | c(b) = c(a|b) holds?

Examples

Conclusion

So in which case c(a) | c(b) => c(a|b) ??
Well: if c(a) = e1 | e2 | ... | en where each "ei" use at most one "a"

Terminology

I don't know what's the terminology for this propriety:
when we have"c" is
c(a) | c(b) !< c(a|b)covariant
c(a) | c(b) !> c(a|b)contravariant
c(a) | c(b) !! c(a|b)? distributive
More: if c(a) | c(b) => c(a|b) 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

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


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 $