Language.TEval.EvalTaglessF

Tagless Typed lambda-calculus with integers and the conditional in the higher-order abstract syntax. Haskell itself ensures the object terms are well-typed. Here we use the tagless final approach.

http://okmij.org/ftp/Computation/Computation.html#teval

Documentation

class Symantics repr where

Methods

l :: (repr t1 -> repr t2) -> repr (t1 -> t2)

a :: repr (t1 -> t2) -> repr t1 -> repr t2

i :: Int -> repr Int

(+:) :: repr Int -> repr Int -> repr Int

ifz :: repr Int -> repr t -> repr t -> repr t

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

Instances

Symantics D

Symantics S

type VarCount = Int

Since we rely on the metalanguage for typechecking and hence type generalization, we have to use `let' of the metalanguage.

It is quite challenging to show terms. Yet, in contrast to the GADT-based approach (EvalTaglessI.hs), we are able to do that, without extending our language with auxiliary syntactic forms. Incidentally, showing of terms is just another way of _evaluating_ them, to strings.

newtype S t

Constructors

S (VarCount -> (String, VarCount))

Instances

Symantics S

newtype D t

We no longer need variables or the environment and we do normalization by evaluation.

Denotational semantics. Why?

Constructors

D t

Instances

Symantics D

evald :: D t -> t

EvalTaglessF> :t term2