Language.TTF

Typed tagless-final interpreters for PCF Higher-order abstract syntax based on the code accompanying the paper by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan

http://okmij.org/ftp/tagless-final/course/course.html#TDPE

Documentation

class Symantics repr where

The language is simply-typed lambda-calculus with fixpoint and constants. It is essentially PCF. The language is just expressive enough for the power function. We define the language by parts, to emphasize modularity. The core plus the fixpoint is the language described in the paper

Hongwei Xi, Chiyan Chen, Gang Chen Guarded Recursive Datatype Constructors, POPL2003

which is used to justify GADTs.

• Core language

Methods

int :: Int -> repr Int

add :: repr Int -> repr Int -> repr Int

lam :: (repr a -> repr b) -> repr (a -> b)

app :: repr (a -> b) -> repr a -> repr b

Instances

Symantics S

Symantics R

ESymantics repr => Symantics (ExtSym repr)

Sample terms and their inferred types

Typed and tagless interpreter

newtype R a

Constructors

R

Fields

unR :: a

Instances

FixSYM R

BoolSYM R

MulSYM R

Symantics R

type VarCounter = Int

• R is not a tag! It is a newtype The expression with unR _looks_ like tag introduction and elimination. But the function unR is *total*. There is no run-time error is possible at all -- and this fact is fully apparent to the compiler. Furthermore, at run-time, (R x) is indistinguishable from x * R is a meta-circular interpreter This is easier to see now. So, object-level addition is _truly_ the metalanguage addition. Needless to say, that is efficient. * R never gets stuck: no pattern-matching of any kind * R is total
• Another interpreter

newtype S a

Constructors

S

Fields

unS :: VarCounter -> String

Instances

FixSYM S

BoolSYM S

MulSYM S

Symantics S

class MulSYM repr where

• The crucial role of repr being a type constructor rather than just a type. It lets some information about object-term representation through (the type) while keeping the representation itself hidden.
• * Extensions of the language
• Multiplication

Methods

mul :: repr Int -> repr Int -> repr Int

Instances

MulSYM S

MulSYM R

Booleans

class BoolSYM repr where

Methods

bool :: Bool -> repr Bool

leq :: repr Int -> repr Int -> repr Bool

if_ :: repr Bool -> repr a -> repr a -> repr a

Instances

BoolSYM S

BoolSYM R

Fixpoint

class FixSYM repr where

Methods

fix :: (repr a -> repr a) -> repr a

Instances

FixSYM S

FixSYM R

Extensions are independent of each other

Extending the R interpreter

Extending the S interpreter