Language.Glambda.Type

Defines types

Glambda types to be used in Haskell terms

data Ty

Representation of a glambda type

Constructors

Arr Ty Ty infixr 1

A function type

IntTy

BoolTy

Instances

Eq Ty

Show Ty

Pretty Ty

readTyCon :: String -> Maybe Ty

Perhaps convert a string representation of a base type into a Ty

Glambda types to be used in Haskell types

data STy :: * -> * where

Singleton for a glambda type

Constructors

SArr :: STy arg -> STy res -> STy (arg -> res) infixr 1

SIntTy :: STy Int

SBoolTy :: STy Bool

Instances

Pretty (STy ty)

data SCtx :: [*] -> * where

Singleton for a typing context

Constructors

SNil :: SCtx []

SCons :: STy h -> SCtx t -> SCtx (h : t) infixr 5

class ITy ty where

An implicit STy, wrapped up in a class constraint

Methods

sty :: STy ty

Instances

ITy Bool

ITy Int

(ITy arg, ITy res) => ITy (arg -> res)

emptyContext :: SCtx []

The singleton for the empty context

refineTy :: Ty -> (forall ty. STy ty -> r) -> r

Convert a Ty into an STy.

unrefineTy :: STy ty -> Ty

Convert an STy into a Ty

eqSTy :: STy ty1 -> STy ty2 -> Maybe (ty1 :~: ty2)

Compare two STys for equality.