2.6. Metatyping

Felix supports a metatyping or kinding system. The reserved identifer TYPE denotes the kind of a type. You can make a function that generates a type from other types. Of course, you can pass these functions to other type functions, and do currying.

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 * TYPE
and 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).

Start C++ section to tut/examples/tut209.flx[1 /1 ]
     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: 
End C++ section to tut/examples/tut209.flx[1]