Last active
September 7, 2025 22:36
-
-
Save takanuva/e6c030518985594eb56f93c9a0be0ac0 to your computer and use it in GitHub Desktop.
Plotkin's CBV CPS translation, de Bruijn index
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| data Term = Var Int | |
| | Abs Term | |
| | App Term Term | |
| deriving Show | |
| lift :: Int -> Int -> Term -> Term | |
| lift i k (Var n) = | |
| Var (if k <= n then i + n else n) | |
| lift i k (Abs e) = | |
| Abs (lift i (1 + k) e) | |
| lift i k (App e f) = | |
| App (lift i k e) (lift i k f) | |
| -- Plotkin's CBV CPS translation | |
| -- Behavior: if n free in t, (1+n) free in [t] | |
| -- Note: The index 0 in [t] is fresh: the cc (here k) | |
| -- Note: cbv (lift i n e) = lift i (1+n) (cbv e) | |
| cbv :: Term -> Term | |
| cbv (Var n) = | |
| -- [x] = k x | |
| App (Var 0) (Var (1 + n)) | |
| cbv (Abs e) = | |
| -- [\x.e] = k (\x.\k.[e]) | |
| -- Where e has a new variable at index 1 (outer k) | |
| App | |
| (Var 0) | |
| (Abs | |
| (Abs | |
| (cbv (lift 1 1 e)))) | |
| cbv (App e f) = | |
| -- [e f] = (\k.[e]) (\g.(\k.[f]) (\v.g v k)) | |
| -- Where e has a new variable at index 0 (outer k) | |
| -- And f has two new variables at index 0 (outer k and g) | |
| App | |
| (Abs (cbv (lift 1 0 e))) | |
| (Abs | |
| (App | |
| (Abs (cbv (lift 2 0 f))) | |
| (Abs | |
| -- (g v) k: (1 0) 2 | |
| (App (App (Var 1) (Var 0)) (Var 2))))) | |
| one = | |
| -- \f.\x.f x | |
| Abs (Abs (App (Var 1) (Var 0))) | |
| one' = | |
| cbv one | |
| main = | |
| print one' |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment