The type evaluator is a specialised version of the typed lambda calculus using eager evaluation. Note that in this calculus, types are values, and their type is TYPE, type functions are also values, with type TYPE->TYPE. Our calculus also supports type tuples of types such as
TYPE * TYPEand values such as
(int, long)Note that (unfortunately) in the abstraction form
fun (t:TYPE):TYPE = { t * t }the curly braces are required, and you can even write:
fun (t:TYPE):TYPE = { return t * t; }as for an ordinary function. This is because Felix uses precisely the same syntax for type functions and ordinary ones; that is, the parser uses the same grammar to build expressions and type expresssions (though each imposes constraints).
1: include "std"; 2: open Long; 3: 4: typedef fun list (elt:TYPE):TYPE => 1 + elt * list elt; 5: 6: typedef fun f(t1:TYPE, t2:TYPE->TYPE) (t3:TYPE): TYPE => (t2 t1) * t3; 7: 8: typedef g = ( 9: fun (t1:TYPE, t2:TYPE->TYPE):TYPE->TYPE => 10: ( fun (t3:TYPE):TYPE => (t2 t1) * t3 ) 11: ) 12: ; 13: 14: 15: // FIXPOINTS WORKING NOW 16: val x : list int = case 1 of list int; 17: 18: typedef fun pair (a:TYPE,b:TYPE):TYPE => a * b; 19: //typedef pair = (fun (a:TYPE,b:TYPE):TYPE => {a * b}); 20: 21: val x2 : (pair (int,long)) = (1,1L); 22: match x2 with 23: | (?a,?b) => { print a; endl; print b; endl; } 24: endmatch; 25: 26: typedef fun twoup (x:TYPE):TYPE => x * x; 27: 28: // (twoup int) * int = (int * int) * int 29: val x3 : (f (int,twoup of (TYPE)) (int)) = ((1,2),3); 30: match x3 with 31: | ((?a,?b),?c) => { print a; endl; print b; endl; print c; endl; } 32: endmatch; 33: