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

Methods

(==) :: Ty -> Ty -> Bool

(/=) :: Ty -> Ty -> Bool

Show Ty

Methods

showsPrec :: Int -> Ty -> ShowS

show :: Ty -> String

showList :: [Ty] -> ShowS

Pretty Ty

Methods

pretty :: Ty -> Doc

prettyList :: [Ty] -> Doc

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)

Methods

pretty :: STy ty -> Doc

prettyList :: [STy ty] -> Doc

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

Minimal complete definition

sty

Methods

sty :: STy ty

Instances

ITy Bool

Methods

sty :: STy Bool

ITy Int

Methods

sty :: STy Int

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

Methods

sty :: STy (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.