LambdaPiToSKUP.hs

LambdaPiToSKUP.hs

{-# 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