Conversion from lambda term to combinatorial term

Question

Suppose there are some data types to express lambda and combinatorial terms:

data Lam α = Var α                   -- v
           | Abs α (Lam α)           -- λv . e1
           | App (Lam α) (Lam α)     -- e1 e2
             deriving (Eq, Show)

infixl 0 :@
data SKI α = V α                     -- x
           | SKI α :@ SKI α          -- e1 e2
           | I                       -- I
           | K                       -- K
           | S                       -- S
             deriving (Eq, Show)

There is also a function to get a list of lambda term's free variables:

fv ∷ Eq α ⇒ Lam α → [α]
fv (Var v) = [v]
fv (Abs x e) = filter (/= x) $ fv e
fv (App e1 e2) = fv e1 ++ fv e2

To convert lambda term to combinatorial term abstract elimination rules could be usefull:

convert ∷ Eq α ⇒ Lam α → SKI α

1) T[x] => x

convert (Var x) = V x

2) T[(E₁ E₂)] => (T[E₁] T[E₂])

convert (App e1 e2) = (convert e1) :@ (convert e2)

3) T[λx.E] => (K T[E]) (if x does not occur free in E)

convert (Abs x e) | x `notElem` fv e = K :@ (convert e)

4) T[λx.x] => I

convert (Abs x (Var y)) = if x == y then I else K :@ V y

5) T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)

convert (Abs x (Abs y e)) | x `elem` fv e = convert (Abs x (convert (Abs y e)))

6) T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])

convert (Abs x (App y z)) = S :@ (convert (Abs x y)) :@ (convert (Abs x z))

convert  _ = error ":["

This definition is not valid because of 5):

Couldn't match expected type `Lam α' with actual type `SKI α'
In the return type of a call of `convert'
In the second argument of `Abs', namely `(convert (Abs y e))'
In the first argument of `convert', namely
  `(Abs x (convert (Abs y e)))'

So, what I have now is:

> convert $ Abs "x" $ Abs "y" $ App (Var "y") (Var "x")
*** Exception: :[

What I want is (hope I calculate it right):

> convert $ Abs "x" $ Abs "y" $ App (Var "y") (Var "x")
S :@ (S (KS) (S (KK) I)) (S (KK) I)

Question:

If lambda term and combinatorial term have a different types of expression, how 5) could be formulated right?

Answer 1

Let's consider the equation T[λx.λy.E] => T[λx.T[λy.E]].

We know the result of T[λy.E] is an SKI expression. Since it has been produced by one of the cases 3, 4 or 6, it is either I or an application (:@).

Thus the outer T in T[λx.T[λy.E]] must be one of the cases 3 or 6. You can perform this case analysis in the code. I'm sorry but I don't have the time to write it out.

Answer 2

Here it's better to have a common data type for combinators and lambda expressions. Notice that your types already have significant overlap (Var, App), and it doesn't hurt to have combinators in lambda expressions.

The only possibility we want to eliminate is having lambda abstractions in combinator terms. We can forbid them using indexed types.

In the following code the type of a term is parameterised by the number of nested lambda abstractions in that term. The convert function returns Term Z a, where Z means zero, so there are no lambda abstractions in the returned term.

For more information about singleton types (which are used a bit here), see the paper Dependently Typed Programming with Singletons.

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs, TypeOperators,
    ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-}

data Nat = Z | Inc Nat

data SNat :: Nat -> * where
  SZ :: SNat Z
  SInc :: NatSingleton n => SNat n -> SNat (Inc n)

class NatSingleton (a :: Nat) where
  sing :: SNat a

instance NatSingleton Z where sing = SZ
instance NatSingleton a => NatSingleton (Inc a) where sing = SInc sing

type family Max (a :: Nat) (b :: Nat) :: Nat
type instance Max Z a = a
type instance Max a Z = a
type instance Max (Inc a) (Inc b) = Inc (Max a b)

data Term (l :: Nat) a where
  Var :: a -> Term Z a
  Abs :: NatSingleton l => a -> Term l a -> Term (Inc l) a
  App :: (NatSingleton l1, NatSingleton l2)
      => Term l1 a -> Term l2 a -> Term (Max l1 l2) a
  I   :: Term Z a
  K   :: Term Z a
  S   :: Term Z a

fv :: Eq a => Term l a -> [a]
fv (Var v) = [v]
fv (Abs x e) = filter (/= x) $ fv e
fv (App e1 e2) = fv e1 ++ fv e2
fv _ = []

eliminateLambda :: (Eq a, NatSingleton l) => Term (Inc l) a -> Term l a
eliminateLambda t =
  case t of
    Abs x t ->
      case t of
        Var y
          | y == x -> I
          | otherwise -> App K (Var y)
        Abs {} -> Abs x $ eliminateLambda t
        App a b -> S `App` (eliminateLambda $ Abs x a)
                     `App` (eliminateLambda $ Abs x b)
    App a b -> eliminateLambdaApp a b

eliminateLambdaApp
  :: forall a l1 l2 l . 
     (Eq a, Max l1 l2 ~ Inc l,
      NatSingleton l1,
      NatSingleton l2)
  => Term l1 a -> Term l2 a -> Term l a
eliminateLambdaApp a b =
  case (sing :: SNat l1, sing :: SNat l2) of
    (SInc _, SZ    ) -> App (eliminateLambda a) b
    (SZ    , SInc _) -> App a (eliminateLambda b)
    (SInc _, SInc _) -> App (eliminateLambda a) (eliminateLambda b)

convert :: forall a l . Eq a => NatSingleton l => Term l a -> Term Z a
convert t =
  case sing :: SNat l of
    SZ -> t
    SInc _ -> convert $ eliminateLambda t