Skip to content

Commit 8e8f02a

Browse files
author
Thomas Mahler
committed
simpler approach
1 parent a54f863 commit 8e8f02a

File tree

3 files changed

+280
-0
lines changed

3 files changed

+280
-0
lines changed

‎lambda-ski.cabal‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ library
3232
CCC.CatExpr
3333
CCC.CCC
3434
CCC.Compiler
35+
CCC.CompilerElliott
3536
CCC.Hask
3637
CCC.Interpreter
3738
CCC.Rewrite
@@ -105,6 +106,7 @@ test-suite lambda-ski-test
105106
main-is: Spec.hs
106107
other-modules:
107108
CCCCompilerSpec
109+
CompilerElliottSpec
108110
GraphReductionSpec
109111
ReducerKiselyovSpec
110112
ReducerSpec

‎src/CCC/CompilerElliott.hs‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
module CCC.CompilerElliott
2+
( Cat (..)
3+
, compile
4+
, absCCC
5+
, eval
6+
, evalTop
7+
, Value (..)
8+
) where
9+
10+
import Parser (Environment, Expr (..))
11+
12+
-- Untyped CCC terms -----------------------------------------------------------
13+
14+
data Cat
15+
= CVar String -- free variable (eliminated by absCCC)
16+
| CId -- id
17+
| CComp Cat Cat -- f . g
18+
| CFst | CSnd -- projections
19+
| CFan Cat Cat -- ⟨f, g⟩ (△)
20+
| CApply -- apply (eval morphism)
21+
| CCurry Cat -- curry f
22+
| CConst Integer -- constant integer
23+
| CAdd | CSub | CMul
24+
| CEql | CLeq | CGeq
25+
| CFix Cat -- fix (step)
26+
deriving (Show, Eq)
27+
28+
-- Compilation: Expr → Cat -----------------------------------------------------
29+
30+
compile :: Environment -> Expr -> Cat
31+
compile _ (Int i) = CConst i
32+
compile env (Var x) = resolveVar env x
33+
compile env (App f a)
34+
| isFixOp env f = compileFix env a
35+
compile env (App f a) = CComp CApply (CFan (compile env f) (compile env a))
36+
compile env (Lam x body) = CCurry (absCCC x (compile env body))
37+
38+
resolveVar :: Environment -> String -> Cat
39+
resolveVar env x = case lookup x env of
40+
Just e -> compile env e
41+
Nothing -> resolvePrim x
42+
43+
resolvePrim :: String -> Cat
44+
resolvePrim "+" = CCurry CAdd
45+
resolvePrim "-" = CCurry CSub
46+
resolvePrim "*" = CCurry CMul
47+
resolvePrim "sub" = CCurry CSub
48+
resolvePrim "sub1" = CCurry (CComp CSub (CFan CSnd (CConst 1)))
49+
resolvePrim "is0" = CCurry (CComp CEql (CFan CSnd (CConst 0)))
50+
resolvePrim "eql" = CCurry CEql
51+
resolvePrim "leq" = CCurry CLeq
52+
resolvePrim "geq" = CCurry CGeq
53+
resolvePrim "true" = CSnd -- Scott TRUE = snd
54+
resolvePrim "false" = CFst -- Scott FALSE = fst
55+
resolvePrim "if" = CCurry (CCurry (CCurry ifBody))
56+
where
57+
-- context: (((env, sel), t), e)
58+
sel = CComp CSnd (CComp CFst CFst) -- selector
59+
t = CComp CSnd CFst -- then branch
60+
e = CSnd -- else branch
61+
ifBody = CComp CApply (CFan sel (CFan e t))
62+
resolvePrim name = CVar name
63+
64+
-- Fixpoint detection ----------------------------------------------------------
65+
66+
isFixOp :: Environment -> Expr -> Bool
67+
isFixOp env = go []
68+
where
69+
go _ (Int _) = False
70+
go _ (Lam _ _) = False
71+
go _ (App _ _) = False
72+
go seen (Var name)
73+
| name == "y" || name == "fix" = True
74+
| name `elem` seen = False
75+
| otherwise = maybe False (go (name : seen)) (lookup name env)
76+
77+
compileFix :: Environment -> Expr -> Cat
78+
compileFix env (Lam self body) =
79+
CFix (CCurry (absCCC self (compile env body)))
80+
compileFix _ _ = error "fix expects a lambda step function"
81+
82+
-- Elliott's bracket abstraction -----------------------------------------------
83+
--
84+
-- The three core rules mirror SKI bracket abstraction:
85+
-- [x] x = snd (cf. I)
86+
-- [x] e = e . fst (x not in e) (cf. K)
87+
-- [x] (f @ g) = apply . ⟨[x] f, [x] g⟩ (cf. S)
88+
--
89+
-- Plus structural rules for Cat constructors that arise from compilation.
90+
91+
absCCC :: String -> Cat -> Cat
92+
-- Core rules:
93+
absCCC x (CVar y) | x == y = CSnd
94+
absCCC x t | not (freeIn x t) = CComp t CFst
95+
absCCC x (CComp CApply (CFan f g)) =
96+
CComp CApply (CFan (absCCC x f) (absCCC x g))
97+
-- Structural rules:
98+
absCCC x (CFan f g) = CFan (absCCC x f) (absCCC x g)
99+
absCCC x (CComp f g) = CComp (absCCC x f) (CFan (absCCC x g) CSnd)
100+
absCCC x (CCurry f) = CCurry (CComp (absCCC x f) assocR)
101+
where
102+
-- assocR : ((ctx, x), y) → ((ctx, y), x)
103+
assocR = CFan (CFan (CComp CFst CFst) CSnd) (CComp CSnd CFst)
104+
absCCC x (CFix f) = CFix (absCCC x f)
105+
absCCC _ t = error $ "absCCC: unexpected term " ++ show t
106+
107+
freeIn :: String -> Cat -> Bool
108+
freeIn x (CVar y) = x == y
109+
freeIn x (CComp f g) = freeIn x f || freeIn x g
110+
freeIn x (CFan f g) = freeIn x f || freeIn x g
111+
freeIn x (CCurry f) = freeIn x f
112+
freeIn x (CFix f) = freeIn x f
113+
freeIn _ _ = False
114+
115+
-- Untyped interpreter ---------------------------------------------------------
116+
117+
data Value
118+
= VInt Integer
119+
| VPair Value Value
120+
| VFun (Value -> Value)
121+
122+
instance Show Value where
123+
show (VInt i) = show i
124+
show (VPair a b) = "(" ++ show a ++ ", " ++ show b ++ ")"
125+
show (VFun _) = "<fun>"
126+
127+
vUnit :: Value
128+
vUnit = VPair (VInt 0) (VInt 0)
129+
130+
evalTop :: Cat -> Integer
131+
evalTop cat = case eval cat vUnit of
132+
VInt i -> i
133+
v -> error $ "evalTop: expected integer, got " ++ show v
134+
135+
eval :: Cat -> Value -> Value
136+
eval CId v = v
137+
eval (CComp f g) v = eval f (eval g v)
138+
eval CFst (VPair a _) = a
139+
eval CSnd (VPair _ b) = b
140+
eval (CFan f g) v = VPair (eval f v) (eval g v)
141+
eval CApply (VPair f x) = applyVal f x
142+
eval (CCurry f) v = VFun (\x -> eval f (VPair v x))
143+
eval (CConst i) _ = VInt i
144+
eval CAdd (VPair (VInt a) (VInt b)) = VInt (a + b)
145+
eval CSub (VPair (VInt a) (VInt b)) = VInt (a - b)
146+
eval CMul (VPair (VInt a) (VInt b)) = VInt (a * b)
147+
eval CEql (VPair (VInt a) (VInt b)) = scottBool (a == b)
148+
eval CLeq (VPair (VInt a) (VInt b)) = scottBool (a <= b)
149+
eval CGeq (VPair (VInt a) (VInt b)) = scottBool (a >= b)
150+
eval (CFix step) v = let rec = VFun (\x -> eval (CFix step) x)
151+
in eval step (VPair rec v)
152+
eval t v = error $ "eval: stuck on " ++ show t ++ " with " ++ show v
153+
154+
scottBool :: Bool -> Value
155+
scottBool True = VFun (\_ -> VFun id) -- TRUE = snd: λt e. e
156+
scottBool False = VFun (\x -> VFun (const x)) -- FALSE = fst: λt e. t
157+
158+
applyVal :: Value -> Value -> Value
159+
applyVal (VFun f) x = f x
160+
applyVal v _ = error $ "applyVal: not a function: " ++ show v

‎test/CompilerElliottSpec.hs‎

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
module CompilerElliottSpec where
2+
3+
import Data.Maybe (fromJust)
4+
import Test.Hspec
5+
6+
import CCC.CompilerElliott (Cat (..), compile, absCCC, eval, evalTop)
7+
import Parser (Expr (..), parseEnvironment)
8+
import TestSources (ackermann, cccAlias, cccConst, cccIdentity,
9+
cccLiteral, factorial, fibonacci, gaussian,
10+
tak)
11+
12+
main :: IO ()
13+
main = hspec spec
14+
15+
spec :: Spec
16+
spec = do
17+
describe "absCCC core rules" $ do
18+
it "[x] x = snd" $
19+
absCCC "x" (CVar "x") `shouldBe` CSnd
20+
21+
it "[x] y = y . fst (x not free)" $
22+
absCCC "x" (CVar "y") `shouldBe` CComp (CVar "y") CFst
23+
24+
it "[x] (apply . <f, g>) = apply . <[x] f, [x] g>" $
25+
absCCC "x" (CComp CApply (CFan (CVar "x") (CVar "x")))
26+
`shouldBe` CComp CApply (CFan CSnd CSnd)
27+
28+
describe "compile + eval" $ do
29+
it "compiles and evaluates an integer literal" $
30+
evalTop (compile [] (Int 42)) `shouldBe` 42
31+
32+
it "compiles and evaluates a variable lookup" $
33+
evalTop (compile [("n", Int 13)] (Var "n")) `shouldBe` 13
34+
35+
it "compiles and evaluates identity application" $
36+
evalTop (compile [] (App (Lam "x" (Var "x")) (Int 7))) `shouldBe` 7
37+
38+
it "compiles and evaluates const function" $
39+
evalTop (compile [] (App (App (Lam "x" (Lam "y" (Var "x"))) (Int 3)) (Int 9)))
40+
`shouldBe` 3
41+
42+
it "compiles and evaluates addition" $
43+
evalTop (compile [] (App (App (Var "+") (Int 3)) (Int 5))) `shouldBe` 8
44+
45+
it "compiles and evaluates subtraction" $
46+
evalTop (compile [] (App (App (Var "-") (Int 10)) (Int 3))) `shouldBe` 7
47+
48+
it "compiles and evaluates multiplication" $
49+
evalTop (compile [] (App (App (Var "*") (Int 4)) (Int 5))) `shouldBe` 20
50+
51+
it "compiles and evaluates sub1" $
52+
evalTop (compile [] (App (Var "sub1") (Int 5))) `shouldBe` 4
53+
54+
it "compiles and evaluates is0 true case" $
55+
evalTop (compile [] (App (App (App (Var "if") (App (Var "is0") (Int 0))) (Int 1)) (Int 2)))
56+
`shouldBe` 1
57+
58+
it "compiles and evaluates is0 false case" $
59+
evalTop (compile [] (App (App (App (Var "if") (App (Var "is0") (Int 5))) (Int 1)) (Int 2)))
60+
`shouldBe` 2
61+
62+
describe "fixpoint (y combinator)" $ do
63+
it "compiles and evaluates factorial 5" $ do
64+
let expr = App (App (Var "y") (Lam "f" (Lam "n"
65+
(App (App (App (Var "if") (App (Var "is0") (Var "n")))
66+
(Int 1))
67+
(App (App (Var "*") (Var "n"))
68+
(App (Var "f") (App (Var "sub1") (Var "n"))))))))
69+
(Int 5)
70+
evalTop (compile [] expr) `shouldBe` 120
71+
72+
it "compiles and evaluates via fix alias" $ do
73+
let expr = App (App (Var "fix") (Lam "f" (Lam "n"
74+
(App (App (App (Var "if") (App (Var "is0") (Var "n")))
75+
(Int 1))
76+
(App (App (Var "*") (Var "n"))
77+
(App (Var "f") (App (Var "sub1") (Var "n"))))))))
78+
(Int 5)
79+
evalTop (compile [] expr) `shouldBe` 120
80+
81+
it "compiles and evaluates multi-arg recursion" $ do
82+
let expr = App (App (App (Var "y") (Lam "f" (Lam "x" (Lam "y" (Var "x"))))) (Int 1)) (Int 2)
83+
evalTop (compile [] expr) `shouldBe` 1
84+
85+
describe "integration with TestSources" $ do
86+
it "evaluates cccLiteral" $
87+
verifyMainMatchesExpected cccLiteral
88+
89+
it "evaluates cccAlias" $
90+
verifyMainMatchesExpected cccAlias
91+
92+
it "evaluates cccIdentity" $
93+
verifyMainMatchesExpected cccIdentity
94+
95+
it "evaluates cccConst" $
96+
verifyMainMatchesExpected cccConst
97+
98+
it "evaluates factorial" $
99+
verifyMainMatchesExpected factorial
100+
101+
it "evaluates fibonacci" $
102+
verifyMainMatchesExpected fibonacci
103+
104+
it "evaluates gaussian" $
105+
verifyMainMatchesExpected gaussian
106+
107+
it "evaluates ackermann" $
108+
verifyMainMatchesExpected ackermann
109+
110+
it "evaluates tak" $
111+
verifyMainMatchesExpected tak
112+
113+
verifyMainMatchesExpected :: String -> Expectation
114+
verifyMainMatchesExpected source = do
115+
let env = parseEnvironment source
116+
mainExpr = fromJust (lookup "main" env)
117+
expectedExpr = fromJust (lookup "expected" env)
118+
evalTop (compile env mainExpr) `shouldBe` evalTop (compile env expectedExpr)

0 commit comments

Comments
 (0)