Various lambda-calculus implementations

0-PHOAS-total-evaluator.hs

-- λ> eval (A (L (\(C i) -> C (i * 2))) (C 2))
-- 4

{-# LANGUAGE GADTs #-}

data E a where
  C :: a -> E a
  L :: (E a -> E b) -> E (a -> b)
  A :: E (a -> b) -> E a -> E b

eval :: E a -> a
eval (L f) = \x -> eval (f (C x))
eval (A e1 e2) = (eval e1) (eval e2)
eval (C v) = v

1-HOAS-Non-total-evaluator.hs

-- Trivial HOAS-based lambda-calculus interpreter/DSL
-- This is most convenient but can't be parsed from an arbitrary
-- string as-is without more work.

data E = A E E | L (E -> E) | C Int

eval (A op x) =
  case eval op of
    L f -> eval (f (eval x))
    t -> error ("not a function " ++ show t)
eval t = t

instance Show E where
  show (A op x) = parens op ++ " " ++ parens x
    where parens y@A{} = "(" ++ show y ++ ")"
          parens y@L{} = "(" ++ show y ++ ")"
          parens y = show y
  show (L _) = "<function>"
  show (C i) = show i

2-HOAS-parser-non-total-evaluator.hs

{-# LANGUAGE OverloadedStrings #-}
import Control.Applicative
import Data.Attoparsec.Text

data E = A E E | L Int (E -> E) | C Int

expr = lam <|> app <|> term
  where lam =
          do string "\\"
             i <- decimal
             string "."
             e <- expr
             return (L i (\x -> sub i x e))
          where sub i x e =
                  case e of
                    C j | i == j -> x
                    A f y -> A (sub i x f) (sub i x y)
                    L j f | i /= j -> L j (\y -> sub i x (f y))
                    _ -> e
        app =
          do op <- parens lam <|> parens app <|> term
             string " "
             arg <- expr
             return (A op arg)
        parens p =
          do string "("
             v <- p
             string ")"
             return v
        term = fmap C decimal

eval (A op x) =
  case eval op of
    L _ f -> eval (f (eval x))
    t -> error ("not a function " ++ show t)
eval t = t

instance Show E where
  show (A op x) = parens op ++ " " ++ parens x
    where parens y@A{} = "(" ++ show y ++ ")"
          parens y@L{} = "(" ++ show y ++ ")"
          parens y = show y
  show (L _ _) = "<function>"
  show (C i) = show i

3-HOAS-non-total-eval-take-two.hs

-- Simple lambda-calculus with ints for terms and vars, which will be
-- converted to HOAS before eval'ing.
-- handles out of scope vars before eval'ing

module HOAS where

data E = A E E | C Int | L Int E | V Int | HL (E -> E)
 
hoas (A op x) = A (hoas op) (hoas x)
hoas (L i e) = HL (\x -> hoas (sub x e))
  where sub x (V j) | j == i = x
        sub x (A op a) = A (sub x op) (sub x a)
        sub x (L j e') | j /= i = L j (sub x e')
        sub x e' = e'
hoas (V i) = error ("var " ++ show i ++ " is not in scope")
hoas t = t
 
add = HL (\(C x) -> HL (\(C y) -> C (x * y)))
 
eval (A op x) =
  case eval op of
    HL f -> eval (f (eval x))
    t -> error ("not a function " ++ show t)
eval t = t
 
instance Show E where
  show (A op x) = parens op ++ " " ++ parens x
    where parens y@A{} = "(" ++ show y ++ ")"
          parens y@L{} = "(" ++ show y ++ ")"
          parens y = show y
  show (L i e) = "λ" ++ show i ++ "." ++ show e
  show (HL _) = "<function>"
  show (C i) = show i
  show (V i) = show i

4-HOAS-intermediate-step.hs

-- Simple lambda-calculus without HOAS and conversion to HOAS step
-- Also type-safe GADT.
-- Also parametrized over the type of value (e.g. E Int or E String),
-- including type-checking in the `hoas' step.
-- hoas step will also throw type errors before eval is ever started.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

module HOAS where

import Data.Typeable

data E a where
  A :: (Typeable a,Typeable b) => E (a -> b) -> E a -> E b
  C :: Int -> E Int
  L :: (Typeable a, Typeable b) => Int -> E b -> E (a -> b)
  V :: Typeable a => Int -> E a
  HL :: (E a -> E b) -> E (a -> b)
  S :: String -> E String

hoas :: Typeable a => E a -> E a
hoas (A op x) = A (hoas op) (hoas x)
hoas (L i e) = HL (\x -> hoas (sub i x e))
hoas (V i) = error ("var " ++ show i ++ " is not in scope")
hoas t = t

sub :: (Typeable a,Typeable b) => Int -> E a -> E b -> E b
sub i x y@(V j)
  | j == i =
    case gcast x of
      Just x' -> x'
      Nothing -> error ("types of " ++ show x ++ " and " ++ show y ++ " don't match")
sub i x (A op a) = A (sub i x op) (sub i x a)
sub i x (L j e') | j /= i = L j (sub i x e')
sub i x e' = e'

add :: E (Int -> Int -> Int)
add = HL (\(C x) -> HL (\(C y) -> C (x * y)))

eval :: E a -> E a
eval (A op x) =
  case eval op of
    HL f -> eval (f (eval x))
    t -> error ("not a function " ++ show t)
eval t = t

instance Show (E a) where
  show (A op x) = parens op ++ " " ++ parens x
    where parens y@A{} = "(" ++ show y ++ ")"
          parens y@L{} = "(" ++ show y ++ ")"
          parens y = show y
  show (L i e) = "λ" ++ show i ++ "." ++ show e
  show (HL _) = "<function>"
  show (C i) = show i
  show (S i) = show i
  show (V i) = show i

5-PHOAS-staged-total-evaluator.hs

-- Lambda-calculus interpreter with type-safe staged
-- separation between non-HOAS and HOAS'd functions.

-- Notice that the eval function has no error cases.

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

module HOAS where

import Data.Typeable

data Dirty
data Clean

data E s a where
  A :: (Typeable a,Typeable b) => E s (a -> b) -> E s a -> E s b
  C :: Int -> E s Int
  L :: (Typeable a, Typeable b) => Int -> E Dirty b -> E Dirty (a -> b)
  V :: Typeable a => Int -> E Dirty a
  HL :: (E Clean a -> E Clean b) -> E Clean (a -> b)
  FFI :: (E Clean a -> E Clean b) -> E Dirty (a -> b)
  S :: String -> E s String

deriving instance Typeable E

hoas :: Typeable a => E Dirty a -> E Clean a
hoas (A op x) = A (hoas op) (hoas x)
hoas (L i e) = HL (\x -> hoas (sub i (dirty x) e))
hoas (V i) = error ("var " ++ show i ++ " is not in scope")
hoas (FFI f) = HL f
hoas (S s) = S s
hoas (C i) = C i

dirty :: E Clean a -> E Dirty a
dirty (C i) = C i
dirty (A op x) = A (dirty op) (dirty x)
dirty (S s) = S s
dirty (HL f) = FFI f

sub :: (Typeable a,Typeable b) => Int -> E Dirty a -> E Dirty b -> E Dirty b
sub i x y@(V j)
  | j == i =
    case gcast x of
      Just x' -> x'
      Nothing -> error ("types of " ++ show x ++ " and " ++ show y ++ " don't match")
sub i x (A op a) = A (sub i x op) (sub i x a)
sub i x (L j e') | j /= i = L j (sub i x e')
sub _ _ e = e

add :: E Dirty (Int -> Int -> Int)
add = FFI (\(C x) -> HL (\(C y) -> C (x * y)))

eval :: E Clean a -> E Clean a
eval (A op x) =
  case op of
    HL f -> eval (f (eval x))
    A op' y' -> eval (A (eval (A op' y')) x)
eval x = x

-- The only cases handled by the above catch-all are:
-- eval (S s) = S s
-- eval (C c) = C c
-- eval (HL l) = HL l
-- (No FFI, or L.)

instance Show (E s a) where
  show (A op x) = parens op ++ " " ++ parens x
    where parens y@A{} = "(" ++ show y ++ ")"
          parens y@L{} = "(" ++ show y ++ ")"
          parens y = show y
  show (L i e) = "λ" ++ show i ++ "." ++ show e
  show (HL _) = "<function>"
  show (FFI _) = "<foreign function>"
  show (C i) = show i
  show (S i) = show i
  show (V i) = show i