Language.Glambda.Exp

The Exp GADT. Glambda expressions encoded in an Exp value are *always* well-typed.

Documentation

data Exp :: [*] -> * -> * where

Exp ctx ty is a well-typed expression of type ty in context ctx. Note that a context is a list of types, where a type's index in the list indicates the de Bruijn index of the associated term-level variable.

Constructors

Var :: Elem ctx ty -> Exp ctx ty

Lam :: Exp (arg : ctx) res -> Exp ctx (arg -> res)

App :: Exp ctx (arg -> res) -> Exp ctx arg -> Exp ctx res

Arith :: Exp ctx Int -> ArithOp ty -> Exp ctx Int -> Exp ctx ty

Cond :: Exp ctx Bool -> Exp ctx ty -> Exp ctx ty -> Exp ctx ty

Fix :: Exp ctx (ty -> ty) -> Exp ctx ty

IntE :: Int -> Exp ctx Int

BoolE :: Bool -> Exp ctx Bool

Instances

Pretty (Exp ctx ty)

PrettyExp (Exp ctx ty)

data Elem :: [a] -> a -> * where

Elem xs x is evidence that x is in the list xs. EZ :: Elem xs x is evidence that x is the first element of xs. ES ev :: Elem xs x is evidence that x is one position later in xs than is indicated in ev

Constructors

EZ :: Elem (x : xs) x

ES :: Elem xs x -> Elem (y : xs) x

class GlamVal t where

Classifies types that can be values of glambda expressions

Associated Types

data Val t

Well-typed closed values. Encoded as a data family with newtype instances in order to avoid runtime checking of values

Methods

val :: Val t -> Exp [] t

Convert a glambda value back into a glambda expression

Instances

GlamVal Bool

GlamVal Int

GlamVal (a -> b)

prettyVal :: Val t -> STy t -> Doc

Pretty-prints a Val. This needs type information to know how to print. Pattern matching gives GHC enough information to be able to find the GlamVal instance needed to construct the PrettyExp instance.

eqExp :: Exp ctx1 ty1 -> Exp ctx2 ty2 -> Bool

Equality on expressions, needed for testing