liboleg-2010.1.10.0: An evolving collection of Oleg Kiselyov's Haskell modules




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 type of trees representing our expressions `on the wire'

Serialized expressions are _untyped_

data Tree Source


Leaf String 
Node String [Tree] 


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


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)

data DynTerm repr h Source


forall a . DynTerm (TQ a) (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

data VarDesc t Source


VarDesc (TQ t) VarName 


Var gamma h => Var (VarDesc t, gamma) (t, h) 

Relating Gamma and h

class Var gamma h | gamma -> h whereSource


findvar :: Symantics repr => VarName -> gamma -> Either String (DynTerm repr h)Source


Var () () 
Var gamma h => Var (VarDesc t, gamma) (t, h) 

asTypeRepr :: t -> repr h t -> repr h tSource

typecheck :: (Symantics repr, Var gamma h) => Tree -> gamma -> Either String (DynTerm repr h)Source

Simple tests

Closed interpreter

newtype CL h a Source




unCL :: forall repr. Symantics repr => repr h a


Main tests

Type-check once, evaluate many times

A few combinators to help build trees