Amulet Type AST "Analysis"

amulet-type-ast.idr

data Type = TName TypeName          -- Foo
          | TVar TypeVar            -- a
          | TLambda TypeVar Type    -- \(a : Type) => b -- not strictly necessary
          | TForAll TypeVar Type    -- \{a : Type) => b
          | TExists TypeVar Type    -- (a : Type ** b)
          | TFunc Type Type         -- a -> b
          | TArrow Constraint Type  -- a => b
          | TInst Type Type         -- a b

type Nat f g = forall a. f a -> g a
Nat f g {a} = f a -> g a
Nat = \(f : Type) => \(g : Type) => \{a : Type} => f a -> g a
Nat = TLambda "f" $ TLambda "g" $ TForAll "a" $ TFunc (TInst (TVar "f") (TVar "a")) (TInst (TVar "g") (TVar "a"))