Center

Page

Web

Wiki

# Examples

Ehc

This page is intended to give an impression of the available features implemented in each version of the series of EH compilers. A more elaborate description can be found in the accompanying documentation.

# EH 1: lambda calculus

The first version implements typed lambda calculus. For example, the following EH program is accepted:

```let  i :: Int
i = 5
in   i

```

The compiler will, when invoked with the above source code give the following annotated pretty printed output:

```let i :: Int
i = 5
{- [ i:Int ] -}
in i

```

# EH 2: monomorphic type inference

The second version implements type inference, but finds monomorphic types only. The following program infers for id :: Int -> Int:

```let  id = \x -> x
in   let  v = id 3
in   id

```

Types may also be specified partially by means of a type wildcard, denoted by `...':

```let  id  ::  ... -> ...
id  =   \x -> x
in   let  f   ::  (Int -> Int) -> ...
f   =   \i -> \v -> i v
v   =   f id 3
in   let  v = f id 3
in   v

```

The type of a wildcard is filled in by the type inferencer, the compiler annotated pretty printed version looks like:

```let id :: Int -> Int
id = \x -> x
{- [ id:Int -> Int ] -}
in let f :: (Int -> Int) -> Int -> Int
f = \i -> \v -> i v
v = f id 3
{- [ v:Int, f:(Int -> Int) -> Int -> Int ] -}
in let v = f id 3
{- [ v:Int ] -}
in v

```

# EH 3: polymorphic type inference

The third version provides polymorphism a la Haskell (with Hindley-Milner type inferencing):

```let id = \x -> x
id2 :: a -> a
id2 = \x -> x
v2 = (id2 3,id2 'x')
in let v = (id 3,id 'x')
in v

```

Polymorphism is inferred or specified explicitly (for polymorphic recursive use). All bindings in a let expression are analysed together as a binding group.

# EH 4: forall and exists everywhere

The fourth versions allows universal and existential quantifiers in a type, at any position in the type. For example, universal quantification on a higher ranked position can be specified explicitly:

```let  f   ::  (forall a . a -> a) -> (Int,Char)
f   =   \i -> (i 3, i 'x')
id  ::  forall a . a -> a
id  =   \x -> x
in   f id

```

The quantifier may be omitted. As a form of syntactic sugar the location of the quantifier is inferred: a universal quantifier for a type variable is placed around the smallest arrowtype containing all occurrences of the type variable.

```let  f   ::  (a -> a) -> (Int,Char)
f   =   \i -> (i 3, i 'x')
id  ::  a -> a
id  =   \x -> x
in   f id

```

Existential types:

```let  id   ::  forall a . a -> a
xy   ::  exists a . (a, a->Int)
xy   =   (3,id)
ixy  ::  (exists a . (a, a->Int)) -> Int
ixy  =   \(v,f) -> f v
xy'  =   ixy xy
pq   ::  exists a . (a, a->Int)
pq   =   ('x',id)							-- ERROR
in   xy'

```

# EH 5: data types

No surprises here:

```let  data List a = Nil | Cons a (List a)
in   let  v =  case Cons 3 Nil of
Nil       -> 5
Cons x y  -> x
in   v
```

# EH 6: kind inference

Kind polymorphism, explicitly specified:

```let  data Eq a b  = Eq (forall f . f a -> f b)
id           = \x -> x
in   let  v =  case Eq id of
Eq f -> f
in   v
```

or inferred:

```let  Eq           ::  k -> k -> *
data Eq a b  =   Eq (forall f . f a -> f b)
id           =   \x -> x
in   let  g =  case Eq id of
(Eq f) -> f
in   g
```

# EH 7: non extensible records

Records with notation for extension, update and selection. Support for extensible records (that is, independence of labels across argument passing to functions) is included in version 10.

```let  r   =   (i = 3, c = 'x', id = \x->x)
s   =   (r | c := 5)
in   let  v = (r.id r.i, r.id r.c)
vi = v.1
in   vi
```

# EH 8: code generation

Code generation for an extended version of GRIN. FFI is supported, but only as much as is required for testing. A rudimentary GRIN interpreter (gri) can be used for testing.

```let data Ordering = LT | EQ | GT
data Bool = False | True
data List a = Nil | Cons a (List a)
in
let foreign import jazy "primAddInt" add :: Int -> Int -> Int
foreign import jazy "primCmpInt" compare :: Int -> Int -> Ordering
gt  = \x -> \y ->
case compare x y of
GT -> True
_  -> False
in
let upto = \m n ->
if gt m n then
Nil
else
Cons m (upto (add m 1) n)
sum = \l ->
case l of
Nil     -> 0
Cons n ns -> add n (sum ns)
in sum (upto 1 10)
```

Grin output:

```module "8-sum"
{ \$_Cons \$_x1~1 \$_x2~2
= { unit (#0/C/\$_Cons 2 \$_x1~1 \$_x2~2)}
; \$_EQ
= { unit (#0/C/\$_EQ 0)}
; \$_False
= { unit (#0/C/\$_False 0)}
; \$_GT
= { unit (#1/C/\$_GT 0)}
; \$_LT
= { unit (#2/C/\$_LT 0)}
; \$_Nil
= { unit (#1/C/\$_Nil 0)}
; \$_True
= { unit (#1/C/\$_True 0)}
= { eval \$_9_0_12_1 ; \(#0/C/\$_Int \$__ \$__9_0_12_1) ->
eval \$_9_0_12_2 ; \(#0/C/\$_Int \$__ \$__9_0_12_2) ->
ffi primAddInt \$__9_0_12_1 \$__9_0_12_2 ; \(#U \$_9_0_12_0) ->
unit (#0/C/\$_Int 1 \$_9_0_12_0)
}
; \$_compare \$_9_0_13_1 \$_9_0_13_2
= { eval \$_9_0_13_1 ; \(#0/C/\$_Int \$__ \$__9_0_13_1) ->
eval \$_9_0_13_2 ; \(#0/C/\$_Int \$__ \$__9_0_13_2) ->
ffi primCmpInt \$__9_0_13_1 \$__9_0_13_2
}
; \$_gt \$_x~5 \$_y~6
= { store (#0/F/\$_compare \$_x~5 \$_y~6) ; \\$_0_66_0~7_0 ->
unit \$_0_66_0~7_0 ; \\$_9_0_21_0 ->
eval \$_9_0_21_0 ; \\$_0_66_0!~8_0 ->
case \$_0_66_0!~8_0 of
{ (#0/C/\$_EQ \$__)
-> { unit \$_False ; \\$_9_0_24_0 ->
eval \$_9_0_24_0
}
; (#1/C/\$_GT \$__)
-> { unit \$_True ; \\$_9_0_26_0 ->
eval \$_9_0_26_0
}
; (#2/C/\$_LT \$__)
-> { unit \$_False ; \\$_9_0_28_0 ->
eval \$_9_0_28_0
}
}
}
; rec
{ \$_sum \$_l~19
= { unit \$_l~19 ; \\$_9_0_30_0 ->
eval \$_9_0_30_0 ; \\$_0_139_0!~21_0 ->
case \$_0_139_0!~21_0 of
{ (#0/C/\$_Cons \$__ \$_n~22_2 \$_ns~22_4)
-> { store (#0/F/\$_sum \$_ns~22_4) ; \\$_5_0_31 ->
store (#0/F/\$_add \$_n~22_2 \$_5_0_31) ; \\$_5_0_29 ->
unit \$_5_0_29 ; \\$_9_0_44_0 ->
eval \$_9_0_44_0
}
; (#1/C/\$_Nil \$__)
-> { unit (#0/C/\$_Int 1 0)}
}
}
}
; rec
{ \$_upto \$_m~13 \$_n~14
= { store (#0/F/\$_gt \$_m~13 \$_n~14) ; \\$_0_99_0~15_0 ->
unit \$_0_99_0~15_0 ; \\$_9_0_54_0 ->
eval \$_9_0_54_0 ; \\$_0_99_0!~16_0 ->
store (#0/C/\$_Int 1 1) ; \\$_9_0_56_1 ->
store (#0/F/\$_add \$_m~13 \$_9_0_56_1) ; \\$_5_0_46 ->
store (#0/F/\$_upto \$_5_0_46 \$_n~14) ; \\$_5_0_44 ->
store (#0/F/\$_Cons \$_m~13 \$_5_0_44) ; \\$_5_0_42 ->
case \$_0_99_0!~16_0 of
{ (#0/C/\$_False \$__)
-> { unit \$_5_0_42 ; \\$_9_0_77_0 ->
eval \$_9_0_77_0
}
; (#1/C/\$_True \$__)
-> { unit \$_Nil ; \\$_9_0_79_0 ->
eval \$_9_0_79_0
}
}
}
}
; \$_5_0_50
= { store (#0/C/\$_Int 1 1) ; \\$_9_0_82_0 ->
store (#0/C/\$_Int 1 10) ; \\$_9_0_82_1 ->
\$_upto \$_9_0_82_0 \$_9_0_82_1
}
; main
= { \$_sum \$_5_0_50}
; apply \$_f_9_0_1_0 \$_a_9_0_1_1
= { case \$_f_9_0_1_0 of
{ (#0/P/1/apply \$_9_0_5_0)
-> { apply \$_9_0_5_0 \$_a_9_0_1_1}
; (#0/P/2/apply)
-> { unit (#0/P/1/apply \$_a_9_0_1_1)}
}
}
; eval \$_9_0_0_0
= { fetch \$_9_0_0_0  ; \\$_9_0_0_1 ->
case \$_9_0_0_1 of
{ (#0/C/\$_Int \$_9_0_2_0)
-> { unit \$_9_0_0_1}
; (#0/C/\$_Char \$_9_0_2_1_0)
-> { unit \$_9_0_0_1}
; (#0/C/\$_Cons \$_9_0_2_2_0 \$_9_0_2_2_1)
-> { unit \$_9_0_0_1}
; (#1/C/\$_Nil)
-> { unit \$_9_0_0_1}
; (#0/C/\$_False)
-> { unit \$_9_0_0_1}
; (#1/C/\$_True)
-> { unit \$_9_0_0_1}
; (#0/C/\$_EQ)
-> { unit \$_9_0_0_1}
; (#1/C/\$_GT)
-> { unit \$_9_0_0_1}
; (#2/C/\$_LT)
-> { unit \$_9_0_0_1}
; (#0/P/1/apply \$_~9_0_5_0)
-> { unit \$_9_0_0_1}
; (#0/P/2/apply)
-> { unit \$_9_0_0_1}
; (#0/F/\$_Cons \$_9_0_3_1 \$_9_0_3_2)
-> { \$_Cons \$_9_0_3_1 \$_9_0_3_2 ; \\$_9_0_3_0 ->
update \$_9_0_0_0 \$_9_0_3_0 ; \() ->
unit \$_9_0_3_0
}
-> { \$_add \$_9_0_3_1_1 \$_9_0_3_1_2 ; \\$_9_0_3_1_0 ->
update \$_9_0_0_0 \$_9_0_3_1_0 ; \() ->
unit \$_9_0_3_1_0
}
; (#0/F/apply \$_9_0_3_2_1 \$_9_0_3_2_2)
-> { apply \$_9_0_3_2_1 \$_9_0_3_2_2 ; \\$_9_0_3_2_0 ->
update \$_9_0_0_0 \$_9_0_3_2_0 ; \() ->
unit \$_9_0_3_2_0
}
; (#0/F/\$_compare \$_9_0_3_3_1 \$_9_0_3_3_2)
-> { \$_compare \$_9_0_3_3_1 \$_9_0_3_3_2 ; \\$_9_0_3_3_0 ->
update \$_9_0_0_0 \$_9_0_3_3_0 ; \() ->
unit \$_9_0_3_3_0
}
; (#0/F/\$_gt \$_9_0_3_4_1 \$_9_0_3_4_2)
-> { \$_gt \$_9_0_3_4_1 \$_9_0_3_4_2 ; \\$_9_0_3_4_0 ->
update \$_9_0_0_0 \$_9_0_3_4_0 ; \() ->
unit \$_9_0_3_4_0
}
; (#0/F/\$_sum \$_9_0_3_5_1)
-> { \$_sum \$_9_0_3_5_1 ; \\$_9_0_3_5_0 ->
update \$_9_0_0_0 \$_9_0_3_5_0 ; \() ->
unit \$_9_0_3_5_0
}
; (#0/F/\$_upto \$_9_0_3_6_1 \$_9_0_3_6_2)
-> { \$_upto \$_9_0_3_6_1 \$_9_0_3_6_2 ; \\$_9_0_3_6_0 ->
update \$_9_0_0_0 \$_9_0_3_6_0 ; \() ->
unit \$_9_0_3_6_0
}
; (#0/F/\$_5_0_50)
-> { \$_5_0_50 ; \\$_9_0_4_0 ->
update \$_9_0_0_0 \$_9_0_4_0 ; \() ->
unit \$_9_0_4_0
}
; (#0/F/\$_EQ)
-> { \$_EQ ; \\$_9_0_4_1_0 ->
update \$_9_0_0_0 \$_9_0_4_1_0 ; \() ->
unit \$_9_0_4_1_0
}
; (#0/F/\$_False)
-> { \$_False ; \\$_9_0_4_2_0 ->
update \$_9_0_0_0 \$_9_0_4_2_0 ; \() ->
unit \$_9_0_4_2_0
}
; (#0/F/\$_GT)
-> { \$_GT ; \\$_9_0_4_3_0 ->
update \$_9_0_0_0 \$_9_0_4_3_0 ; \() ->
unit \$_9_0_4_3_0
}
; (#0/F/\$_LT)
-> { \$_LT ; \\$_9_0_4_4_0 ->
update \$_9_0_0_0 \$_9_0_4_4_0 ; \() ->
unit \$_9_0_4_4_0
}
; (#0/F/\$_Nil)
-> { \$_Nil ; \\$_9_0_4_5_0 ->
update \$_9_0_0_0 \$_9_0_4_5_0 ; \() ->
unit \$_9_0_4_5_0
}
; (#0/F/\$_True)
-> { \$_True ; \\$_9_0_4_6_0 ->
update \$_9_0_0_0 \$_9_0_4_6_0 ; \() ->
unit \$_9_0_4_6_0
}
; (#0/F/main)
-> { main ; \\$_9_0_4_7_0 ->
update \$_9_0_0_0 \$_9_0_4_7_0 ; \() ->
unit \$_9_0_4_7_0
}
}
}
}
ctags
{ \$_Int = \$_Int 0 1; \$_Char = \$_Char 0 1; \$_List = \$_Cons 0 2 | \$_Nil 1 0; \$_Bool = \$_False 0 0 | \$_True 1 0; \$_Ordering = \$_EQ 0 0 | \$_GT 1 0 | \$_LT 2 0}
evalmap
{ #0/C/\$Int 1 -> unit; #0/C/\$Char 1 -> unit; #0/C/\$Cons 2 -> unit; #1/C/\$Nil 0 -> unit; #0/C/\$False 0 -> unit; #1/C/\$True 0 -> unit; #0/C/\$EQ 0 -> unit; #1/C/\$GT 0 -> unit; #2/C/\$LT 0 -> unit; #0/P/1/\$apply 1 -> unit; #0/P/2/\$apply 0 -> unit; #0/F/\$Cons 2 -> \$Cons; #0/F/\$add 2 -> \$add; #0/F/\$apply 2 -> \$apply; #0/F/\$compare 2 -> \$compare; #0/F/\$gt 2 -> \$gt; #0/F/\$sum 1 -> \$sum; #0/F/\$upto 2 -> \$upto; #0/F/\$5_0_50 0 -> \$5_0_50; #0/F/\$EQ 0 -> \$EQ; #0/F/\$False 0 -> \$False; #0/F/\$GT 0 -> \$GT; #0/F/\$LT 0 -> \$LT; #0/F/\$Nil 0 -> \$Nil; #0/F/\$True 0 -> \$True; #0/F/\$main 0 -> \$main}
applymap
{ #0/P/1/\$apply 1 -> \$apply; #0/P/2/\$apply 0 -> #0/P/1/\$apply}
```

# EH 9: explicit implicitness, classes

Explicit construction and passing of dictionary:

```let  data List a = Nil | Cons a (List a)                                            -- (1)
data Bool = False | True
not :: Bool -> Bool
not = ...
class Eq a where
eq :: a -> a -> Bool
ne :: a -> a -> Bool
instance dEqInt <: Eq Int where                                                -- (2)        eq = ...        ne = \x y -> not (eq x y)
in
let  filter  ::  (a -> Bool) -> List a -> List a
filter  =   ...
nub     ::  Eq a => List a -> List a
nub     =   \xx ->  case xx of
Nil        -> Nil
Cons x xs  -> Cons x (nub (filter (ne x) xs))
in   nub  (! (dEqInt | eq := ...) <: Eq Int !)                            -- (3)           (Cons 3 (Cons 3 (Cons 4 Nil)))   ```

Higher order predicates:

```let  data Bit        = Zero  | One
data List a     = Nil   | Cons a (List a)
data GRose f a  = GBranch a (f (GRose f a))
concat :: List a -> List a -> List a
in   let  class Binary a where
showBin :: a -> List Bit
instance dBI <: Binary Int where             showBin  = ...           instance dBL <: Binary a => Binary (List a) where
showBin  = ...
instance (Binary a, (Binary b => Binary (f b)))
=> Binary (GRose f a) where
showBin  =  \(GBranch x ts)
-> concat (showBin x) (showBin ts)
in   let  v1 = showBin (GBranch 3 Nil)
in   v1
```

# EH 10: extensible records

```let  add  ::  Int -> Int -> Int
f    ::  (r\x, r\y) => (r|x :: Int,y :: Int) -> Int
f    =   \r -> add r.x r.y
in
let  v1 = f (x = 3, y = 4)
v2 = f (y = 5, a = 'z', x = 6)
in   v2
```

Tuple access, but independent of tuple arity:

```let  snd = \r -> r.2
in
let  v1  = snd (3,4)
v2  = snd (3,4,5)
in   v2
```

-- AtzeDijkstra - 24 Nov 2004