WebHome
- UHC
- EHC
- Documentation
- Features & Status
- EH examples
- Feedback
- News
- FAQ
Related
- Ruler
- Shuffle
- uulib & uuagc
Old Stuff
- Previous WebHome
- AFP2004
Center
Master Program
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)}
; $_add $_9_0_12_1 $_9_0_12_2
= { 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
}
; (#0/F/$_add $_9_0_3_1_1 $_9_0_3_1_2)
-> { $_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
Polymorphic (in remaining labels) access to fields:
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