You are here: UUCS>Ehc Web>Download>Examples (27 Nov 2007, UnknownUser)EditAttach

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 followingannotated 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, denotedby `...':

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

 

-- AtzeDijkstra - 24 Nov 2004
Topic revision: r3 - 27 Nov 2007, UnknownUser
 

This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS? Send feedback