TTyped

TTyped is a simple typed language, consisting of only function definitions. It is loosely based on System F. It consists entirely of a series of function definitions. Each definition has the general form of

name args : type = expr ;

Notes

• Every symbol in a function type is assumed to be polymorphic.

• All functions are curried.

• -> and →, are both parsed the same.

Examples

id x : a -> a = x ;

const x y : a -> b -> a = x ;

one f x : (a -> a) -> a -> a = f x ;

add m n f x : ((a -> a) -> a -> a)
           -> ((a -> a) -> a -> a)
           -> (a -> a) -> a -> a
  = m f (n f x)

EBNF

fundec = sym , {sym} , ":" , type , "=" , expr , ";" ;

expr = expr' , { expr' } ;

expr' = sym
      | "(" , expr , ")" ;

type = type' , { "->" , type' } ;

type' = sym
      | "(" , type , ")" ;

sym = alpha , {alpha | digit} ;

External resources

• An implementation on GitHub