Nameless.hs

-- * Stuff

{-# LANGUAGE DataKinds, RankNTypes, NoMonomorphismRestriction, GADTs, StandaloneDeriving, ScopedTypeVariables #-}

module Nameless where

import Prelude hiding (abs)

-- * Pictures

-- #+BEGIN_SRC ditaa


--                  p                          p       
--                  |                          |
--                  |                          |
--              +---+---+                  +---+---+
--              |  app  |                  |  abs  |
--              +-/---\-+                  +-/---\-+
--               /     \                    /     \
--              /       \                  o       \
--             /         \                          \
--            Lp          Rp                         Rp


-- -- \x. f x

-- -- (\x . \y1 . x) y ---> \y1 . y

-- -- #+END_SRC

-- * Places

data Place = L Place | R Place | Root

data Place' pl where
  L' :: Place' pl -> Place' (L pl)
  R' :: Place' pl -> Place' (R pl)
  Root' :: Place' Root

deriving instance Show (Place' pl)

class KnownPlace pl where
  place :: Place' pl

instance KnownPlace pl => KnownPlace (L pl) where place = L' place
instance KnownPlace pl => KnownPlace (R pl) where place = R' place
instance KnownPlace Root where place = Root'

-- * Lambda Calculus has 2 features

-- Which are /abstraction/ and /application/. We get variables
-- for free from Haskell (i.e. HOAS).

class Lam rep where
  abs :: KnownPlace pl => ((forall use . rep (L pl) use) -> rep d (R pl)) -> rep pl pl
  app :: rep d (L pl) -> rep e (R pl) -> rep pl pl

-- * Examples

-- ** I, K combinator: ~const c _ = c~

-- Ignore second argument and return the first

exConst = abs (\x -> abs (\y -> x))

-- Identity

ixId = abs (\x -> x)

-- (Repeated) Application

ex1 = exConst `app` exConst `app` exConst

-- Self-application under lambda

exSelf = abs (\x -> x `app` x)

-- * Instantiate

-- =Concr= is a candidate representation of lambda terms that
-- can be Shown.

data Concr de pl where
  Abs :: KnownPlace pl => ((forall use . Concr (L pl) use) -> Concr d (R pl)) -> Concr pl pl
  App :: Concr d (L pl) -> Concr e (R pl) -> Concr pl pl
  Dummy :: KnownPlace d => Concr d pl


instance Lam Concr where abs = Abs; app = App

instance Show (Concr de pl) where
  show (App l r) = "(" ++ show l ++ " `app` " ++ show r ++ ")"
  show (Abs f) = "abs (\\" ++ show dummy ++ " -> " ++ show (f dummy) ++ ")"
    where dummy :: Concr (L pl) use
          dummy = Dummy
  show Dummy = short (place :: Place' de)
    where short = ('d':) . clean . show
          clean (' ':rest) = clean rest
          clean ('\'':rest) = clean rest
          clean ('(':rest) = clean rest
          clean (')':rest) = clean rest
          clean ('R':'o':'o':'t':rest) = clean rest
          clean (c:rest) = c : clean rest
          clean "" = ""

-- a little helper

root :: Lam rep => (forall pl . KnownPlace pl => rep pl pl) -> rep Root Root
root = id

-- the same one for Concr

rootConcr :: (forall pl . KnownPlace pl => Concr pl pl) -> Concr Root Root
rootConcr = root