Lambda calculus to SKI combinators calculus compiler

Combinator.hs

module Combinator where

-- https://crypto.stanford.edu/~blynn/lambda/sk.html
-- http://okmij.org/ftp/tagless-final/ski.pdf
-- https://www.cantab.net/users/antoni.diller/brackets/intro.html

import Data.List

type Name = String

data Expr
  = App Expr Expr
  | Lam Name Expr
  | Var Name
  deriving Show

data SK
  = App' SK SK
  | S
  | K
  | I
  | Var' Name
  deriving Show

compile :: Expr -> SK
compile (App e1 e2) = App' (compile e1) (compile e2)
compile (Lam x e) = abstract x (compile e)
compile (Var x) = Var' x

abstract :: Name -> SK -> SK
abstract x = go
  where
  go (App' e1 e2) = App' (App' S (go e1)) (go e2)
  go (Var' y) | x == y = I
  go x = App' K x

Maybe.hs

module Maybe where

data Lam a
  = Var a
  | Lam (Lam (Maybe a))
  | App (Lam a) (Lam a)
  deriving (Eq, Show)

data Comb a
  = S
  | K
  | I
  | B
  | C
  | V a
  | A (Comb a) (Comb a)
  deriving (Eq, Foldable, Functor, Show, Traversable)

infixl 1 @

(@) :: Comb a -> Comb a -> Comb a
(@) = A

compile :: Lam a -> Comb a
compile (Var x) = V x
compile (Lam b) = abstract (compile b)
compile (App f a) = compile f @ compile a

abstract :: Comb (Maybe a) -> Comb a
abstract (A f a) =
  case (sequence f, sequence a) of
    (Nothing, Nothing) -> S @ abstract f @ abstract a
    (Just f, Nothing) -> B @ f @ abstract a
    (Nothing, Just a) -> C @ abstract f @ a
    (Just f, Just a) -> K @ (f @ a)
abstract t = maybe I (K @) (sequence t)