Language.TypeCheck
Contents
- Data type of trees representing our expressions `on the wire'
- Serialized expressions are _untyped_
- Expression format (extensible)
- Node Int [Leaf number] -- int literal
- Node Add [e1,e2] -- addition
- Node App [e1,e2] -- application
- Node Var [Leaf name]
- Node Lam [Leaf name,e1,e2] -- e2 is body, e1 is type of var
- ...
- Format of types
- Node TInt [] -- Int
- Node TArr [e1,e2] -- e1 -> e2
- ...
- Serialized expressions are in the Church-style
- Desiderata
- Type check once, interpret many times
- detect type-checking error _before_ evaluation
- Avoiding read-show problem
- Typing dynamic typing
- Type-safe cast
- data DynTerm repr h = forall a. (Show a, Typeable a) => DynTerm (repr h a)
- De-serialize type expressions
- Error monad, to report deserialization errors
- A few explanations are in order
- Type checking environment
- typecheck :: Symantics repr =>
- Tree -> Either String (DynTerm h repr)
- Open terms may legitimately occur
- typecheck :: Symantics repr =>
- Tree -> Gamma -> Either String (DynTerm h repr)
- Gamma is a compile-time environment: contains variable names
- h is a run-time environment: contains values
- Relating Gamma and h
- Simple tests
- Closed interpreter
- Main tests
- Type-check once, evaluate many times
- A few combinators to help build trees
Description
Why all these extensions? I could've cheated a bit and gotten by without the last four: the function typecheck below is partial anyway. If we permit one sort of errors (when the deserialized term is ill-typed), we may as well permit another sort of errors (a closed-looking term turns out open), even if the latter sort of error can't arise if our typecheck function is correct. due to the desire to let GHC check some correctness properties I wanted to avoid unnecessary errors and let GHC see the correctness of my code to a larger extent
- data Tree
- data DynTerm repr h = forall a . DynTerm (TQ a) (repr h a)
- read_t :: Tree -> Either String Typ
- type VarName = String
- data VarDesc t = VarDesc (TQ t) VarName
- class Var gamma h | gamma -> h where
- asTypeRepr :: t -> repr h t -> repr h t
- typecheck :: (Symantics repr, Var gamma h) => Tree -> gamma -> Either String (DynTerm repr h)
- newtype CL h a = CL {}
Data type of trees representing our expressions `on the wire'
Serialized expressions are _untyped_
Expression format (extensible)
Node Int [Leaf number] -- int literal
Node Add [e1,e2] -- addition
Node App [e1,e2] -- application
Node Var [Leaf name]
Node Lam [Leaf name,e1,e2] -- e2 is body, e1 is type of var
...
Format of types
Node TInt [] -- Int
Node TArr [e1,e2] -- e1 -> e2
...
Serialized expressions are in the Church-style
Desiderata
Type check once, interpret many times
detect type-checking error _before_ evaluation
Avoiding read-show problem
Typing dynamic typing
Type-safe cast
data DynTerm repr h = forall a. (Show a, Typeable a) => DynTerm (repr h a)
De-serialize type expressions
Error monad, to report deserialization errors
A few explanations are in order
Type checking environment
typecheck :: Symantics repr =>
Tree -> Either String (DynTerm h repr)
Open terms may legitimately occur
typecheck :: Symantics repr =>
Tree -> Gamma -> Either String (DynTerm h repr)
Gamma is a compile-time environment: contains variable names
h is a run-time environment: contains values
Relating Gamma and h
asTypeRepr :: t -> repr h t -> repr h tSource