{-# OPTIONS -W #-}
{-# LANGUAGE TypeFamilies, NoMonomorphismRestriction #-}
-- Embedding of a higher-order language
-- The main feature is the presence of binding
-- (e.g., logical quantification).
-- We use a pure lambda calculus here, before
-- getting to the predicate logic
module Lambda where
-- First, we define the syntax of lambda-calculus
class Lambda lrepr where
app :: lrepr (a -> b) -> lrepr a -> lrepr b
lam :: (lrepr a -> lrepr b) -> lrepr (a -> b)
-- Examples
identity = lam (\x -> x)
twice = lam (\f -> lam (\x -> app f (app f x)))
twicetwice = app twice twice
-- The first interpretation (semantics)
-- Interpret lambda-terms as Haskell terms (functions)
data R a = R { unR :: a }
instance Lambda R where
app (R f) (R x) = R (f x)
lam f = R (\x -> unR (f (R x)))
idR = unR identity "hello"
twR = unR twice (+1) 0
ttR = unR twicetwice (+1) 0
-- The second interpretation: showing lambda-terms
-- We can ``see functions''
-- The alias VarCounter should tell the intended meaning:
-- the counter to make variable names.
type VarCounter = Int
data C a = C { unC :: VarCounter -> String }
instance Lambda C where
app (C f) (C x) = C (\i -> "(" ++ f i ++ " " ++ x i ++ ")")
lam f = C (\i -> let x = "x" ++ show i
body = unC (f (C (\_ -> x))) (i + 1)
in "L" ++ x ++ ". " ++ body)
showL (C x) = x 0
idC = showL identity
twC = showL twice
ttC = showL twicetwice
-- We can see abstractions!
-- Some terms are big (twicetwice) and have obvious
-- beta-redices. Can we simplify them before displaying?
type family Known (lrepr :: * -> *) (a :: *)
type instance Known lrepr (a -> b) = P lrepr a -> P lrepr b
data P lrepr a = P { unP :: lrepr a, known :: Maybe (Known lrepr a) }
instance (Lambda lrepr) => Lambda (P lrepr) where
app (P _ (Just f)) x = f x
app (P f Nothing) (P x _) = P (app f x) Nothing
lam f = P (lam (\x -> unP (f (P x Nothing)))) (Just f)
idP = showL . unP $ identity
twP = showL . unP $ twice
ttP = showL . unP $ twicetwice
-- ttP looks much better than ttC
-- Haskell is indeed lambda-calculuator.
-- Not only it does reductions, it also shows the result.