-
Notifications
You must be signed in to change notification settings - Fork 8
/
UntypedLambda.hs
101 lines (81 loc) · 3.08 KB
/
UntypedLambda.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
{-|
Module : Untyped Lambda-Calculus
Description : Syntax and reductions of the untyped lambda-calculus using the Nominal package
Copyright : (c) Murdoch J. Gabbay, 2020
License : GPL-3
Maintainer : murdoch.gabbay@gmail.com
Stability : experimental
Portability : POSIX
Untyped lambda-calculus: syntax, substitution, nominal-style recursion, weak head normal form function, and a couple of examples.
Compare with an example in <https://hackage.haskell.org/package/bound the Bound package>.
-}
{-# LANGUAGE InstanceSigs
, DeriveGeneric
, LambdaCase
, MultiParamTypeClasses
, DeriveAnyClass -- to derive 'Swappable'
, DeriveDataTypeable -- to derive 'Data'
, FlexibleInstances
#-}
module Language.Nominal.Examples.UntypedLambda
(
Var, Exp (..), whnf, lam, example1, example1whnf, example2, example2whnf
)
where
import GHC.Generics
import Data.Generics hiding (Generic, typeOf)
import Language.Nominal.Utilities
import Language.Nominal.Name
import Language.Nominal.Nom
import Language.Nominal.Binder
import Language.Nominal.Abs
import Language.Nominal.Sub
-- | Variables are string-labelled names
type Var = Name String
infixl 9 :@
-- | Terms of the untyped lambda-calculus
data Exp = V Var -- ^ Variable
| Exp :@ Exp -- ^ Application
| Lam (KAbs Var Exp) -- ^ Lambda, using abstraction-type
deriving (Eq, Generic, Data, Swappable) -- , Show)
-- | helper for building lambda-abstractions
lam :: Var -> Exp -> Exp
lam x a = Lam (x @> a)
-- | Substitution. Capture-avoidance is automatic.
instance KSub Var Exp Exp where
sub :: Var -> Exp -> Exp -> Exp
sub v t = rewrite $ \case -- 'rewrite' comes from Scrap-Your-Boilerplate generics. It recurses properly under the binder.
V v' | v' == v -> Just t -- If @V v'@, replace with @t@ ...
_ -> Nothing -- ... otherwise recurse.
{- The substitution instance above is equivalent to the following:
-- | Explicit recursion.
expRec :: (Var -> a) -> (Exp -> Exp -> a) -> (Var -> Exp -> a) -> Exp -> a
expRec f0 _ _ (V n) = f1 n
expRec _ f1 _ (s1 :@ s2) = f2 s1 s2
expRec _ _ f2 (Lam x') = f3 `genApp` x'
instance KSub Var Exp Exp where
sub :: Var -> Exp -> Exp -> Exp
sub v t = expRec (\v' -> if v' == v then t else V v')
(\a b -> sub v t a :@ sub v t b)
(\v' a -> lam v' $ sub v t a)
-}
-- | weak head normal form of a lambda-term.
whnf :: Exp -> Exp
whnf (Lam b' :@ a) = whnf $ b' `conc` a
whnf e = e
-- | (\x x) y
example1 :: Exp
example1 = (\[x, y] -> lam x (V x) :@ V y) `genAppC` freshNames ["x", "y"]
-- | y
example1whnf :: Exp
example1whnf = whnf example1
-- | (\x xy) x
example2 :: Exp
example2 = (\[x, y] -> lam x (V x :@ V y) :@ V x) `genAppC` freshNames ["x", "y"]
-- | xy
example2whnf :: Exp
example2whnf = whnf example2
instance Show Exp where
show (V v) = show v
show (Lam e) = "(λ" ++ (show e) ++ ")"
show (e :@ e') = (show e) ++ " " ++ (show e')