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




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 GADT: This file is not in Haskell98



data Term t whereSource


V :: t -> Term t 
L :: (Term t1 -> Term t2) -> Term (t1 -> t2) 
A :: Term (t1 -> t2) -> Term t1 -> Term t2 
I :: Int -> Term Int 
:+ :: Term Int -> Term Int -> Term Int 
IFZ :: Term Int -> Term t -> Term t -> Term t 
Fix :: Term ((a -> b) -> a -> b) -> Term (a -> b) 


Show (Term t)

Since we rely on the metalanguage for typechecking and hence type generalization, we have to use the metalanguage `let' The (V n) term, aka the polymorphic lift, is not used in user terms. This is the internal component for the sake of evald only (evalo doesn't need it).

It is quite challenging to show terms. In fact, we can't do it for lambda-terms at all! The argument of the L constructor is a function. We can't show functions; if we find a term to apply the function to, we obtain a term, which we can show then. The only candidate for the term to pass to the body of L is the V term; but to construct (V x) we need x -- the value of some type (and we don't have an idea of the type). So, the best we can do is (V undefined) -- which, alas, we can't show. The only solution is to modify the definition of Term t, and make the V constructor thusly: V :: t -> String -> Term t. In that case, we can show V-term values.

evald :: Term t -> tSource

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

Denotational semantics. Why?

evalo :: Term t -> Term tSource

Operational semantics. Why? GADT are still implemented imperfectly: we the default case in case statements (with cannot happen error), to avoid the warning about inexhaustive pattern match -- although these case-brances can never be executed. Why?

EvalTaglessI> :t term2