Created
September 13, 2019 13:03
-
-
Save zelinskiy/7aa4e57dc6b8671a039beefdcfebb9cd to your computer and use it in GitHub Desktop.
LambdaPiToSKUP.hs
This file contains 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
{-# LANGUAGE DeriveFunctor #-} | |
-- https://stackoverflow.com/questions/11406786/what-is-the-combinatory-logic-equivalent-of-intuitionistic-type-theory | |
data SKUP = S | K | U | P deriving (Show, Eq) | |
data Unty a | |
= C SKUP | |
| Unty a :. Unty a | |
| V a | |
deriving (Functor, Eq, Show) | |
infixl 4 :. | |
data Tm a | |
= Var a | |
-- Lam is the only place where binding happens | |
| Lam (Tm a) (Tm (Su a)) | |
| Tm a :$ Tm a | |
-- the second arg of Pi is a function computing a Set | |
| Pi (Tm a) (Tm a) | |
| Set | |
deriving (Show, Functor) | |
infixl 4 :$ | |
data Ze | |
data Su a = Ze | Su a deriving (Show, Functor, Eq) | |
magic :: Ze -> a | |
magic x = x `seq` error "Tragic!" | |
-- Evaluation of combinators | |
eval :: Unty a -> Unty a | |
eval (f :. a) = eval f $. a | |
eval c = c | |
-- requires first arg in normal form | |
($.) :: Unty a -> Unty a -> Unty a | |
-- S f a g = f g (a g) (share environment) | |
C S :. f :. a $. g = f $. g $. (a :. g) | |
-- K a g = a (drop environment) | |
C K :. a $. g = a | |
-- guarantees output in normal form | |
n $. g = n :. eval g | |
infixl 4 $. | |
-- Translating lambda to combinators | |
tm :: Tm a -> Unty a | |
tm (Var a) = V a | |
tm (Lam _ b) = bra (tm b) | |
tm (f :$ a) = tm f :. tm a | |
tm (Pi a b) = C P :. tm a :. tm b | |
tm Set = C U | |
-- binds a variable, building a function | |
bra :: Unty (Su a) -> Unty a | |
-- the variable itself yields the identity | |
bra (V Ze) = C S :. C K :. C K | |
-- free variables become constants | |
bra (V (Su x)) = C K :. V x | |
-- combinators become constant | |
bra (C c) = C K :. C c | |
-- S is exactly lifted application | |
bra (f :. a) = C S :. bra f :. bra a |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment