type ** : Type -> Type -> Type;

var a < c

var {a} : c -> d

class Monad < Type -> Type;

type a : Monad := \ t . t -> t;

free type

Term ::= Var Variable | Lam Variable Term | App Term Term;

type WNet = {(sys, i, o) : T * T * T . i = o};

var a : +Type

var -

var []+

op a : ? b;

op a : ? b;