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

Language.TTFdB

Contents

Description

  • Essentially, Haskell98! * Typed tagless-final interpreters for simply-typed lambda-calculus * de Bruijn indices based on the code accompanying the paper by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan

Synopsis

Abstracting over the final interpreter in IntroHOIF.hs

class Symantics repr whereSource

Methods

int :: Int -> repr h IntSource

add :: repr h Int -> repr h Int -> repr h IntSource

z :: repr (a, h) aSource

s :: repr h a -> repr (any, h) aSource

lam :: repr (a, h) b -> repr h (a -> b)Source

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

Like GADT-based, but in lower-case

Like ExpSYM, but repr is of kind * -> * -> *

The types read like the rules of minimal logic

Type system of simply-typed lambda-calculus in Haskell98!

``a way to write a typed fold function over a typed term.''

Sample terms and their inferred types

td2a = app (int 1) (int 2)

Embedding all and only typed terms of the object language

in the typed metalanguage

Typed and tagless evaluator

object term ==> metalanguage value

newtype R h a Source

Constructors

R 

Fields

unR :: h -> a
 

Instances

R is not a tag!

R is a meta-circular interpreter

R never gets stuck: no variant types, no pattern-match failure

Well-typed programs indeed don't go wrong!

R is total

The instance R is a constructive proof of type soundness

R _looks_ like a reader monad (but h varies)

newtype S h a Source

Constructors

S 

Fields

unS :: [String] -> String
 

Instances