Kinding SystemΒΆ
Felix has a basic kinding system. There is one builtin kind, namely TYPE, the kind of all types.
There are two kind constructors. The infix binary function constructor -> can be used to denote the kind of a type function. The chained non-associative n-ary product constructor * can be used to denote the kind of a type tuple.
Kinds are required in some circumstances, for example Monads are parametrised by a type function:
class Monad [M: TYPE->TYPE] {
virtual fun ret[a]: a -> M a;
virtual fun bind[a,b]: M a * (a -> M b) -> M b;
fun join[a] (n: M (M a)): M a => bind (n , (fun (x:M a):M a=>x));
}
A suitable function is:
typedef fun opt_f (T: TYPE): TYPE => opt[T];
which has kind:
TYPE -> TYPE
A kind annotation can be used with a type variable in a polymorphic specification, if omitted it defaults to TYPE. Types also are implicitly kinded as TYPE.
When a list of type variables is given separated by commas each type is implicitly kinded as TYPE and the whole list is implicitly kinded as a type tuple. For example in
fun f(T,U] (x:T,y:U) => x,y;
the type variable list T,U has kind
TYPE * TYPE
Two more kinds will be introduced in the future:
BOOL
INT
These are the kinds of compile time booleans and integers, respectively.