Initial attempt at lambda expression data structure

OldExp.hs

-- |
-- Module      : Saliva.Model.OldExp
-- Copyright   : GPLv3
--
-- Maintainer  : [email protected]
-- Portability : portable
--
-- The 'Exp' data type, for representing lambda expressions.

module Saliva.Model.OldExp
    (
    -- * Types
      Nat
    , Exp
    ) where

-- | A non-negative number.
--
-- I'll eventually switch to Peano numerals for this, but we can live
-- with plain ints for now.
type Nat = Int

-- | A lambda expression.
data Exp
    -- | Reference to an argument, as a zero-based De Bruijn index.
    = Ref Nat
    -- | Lambda abstraction.
    | Lam Exp
    -- | Function application.
    | App Exp Exp
    deriving (Eq, Show)

-- | Shift all the free variables down by one. Any values that fall
-- below zero are replaced with the supplied value.
shiftDown :: Exp -- ^ Replacement value
          -> Exp -- ^ Expression to shift
          -> Exp
shiftDown = go 0
  where
    go k v exp = case exp of
        Ref n
            | n <  k -> Ref n
            | n == k -> v
            | n  > k -> Ref (pred n)
        Lam e   -> Lam (go (succ k) (shiftUp v) e)
        App x y -> App (go k v x) (go k v y)

-- | Shift all the free variables up by one.
shiftUp :: Exp -- ^ Expression to shift
        -> Exp
shiftUp = go 0
  where
    go k exp = case exp of
        Ref n
            | n <  k -> Ref n
            | n >= k -> Ref (succ n)
        Lam e   -> Lam (go (succ k) e)
        App x y -> App (go k x) (go k y)

evalHNF :: Exp -> Exp
evalHNF exp = case exp of
    Ref n         -> Ref n
    Lam e         -> Lam (evalHNF e)
    App (Lam e) v -> shiftDown v e
    App x       y -> App (evalHNF x) (evalHNF y)

r0, r1, r2 :: Exp
r0 = Ref 0
r1 = Ref 1
r2 = Ref 2

λ, λλ, λλλ :: Exp -> Exp
λ = Lam
λλ = Lam . Lam
λλλ = Lam . Lam . Lam

infixl 2 !
(!) :: Exp -> Exp -> Exp
(!) = App

s, k, i, y :: Exp
s = λλλ ((r2 ! r0) ! (r1 ! r0))
k = λλ r1
i = λ r0

y = λ (inner ! inner)
  where
    inner = λ (r1 ! (r0 ! r0))

church :: Int -> Exp
church n
    | n < 0 = error "Church numerals cannot be negative"
    | otherwise = λλ (foldr (!) r0 (replicate n r1))