-- Language implementation bakeoff:
-- Coquand-Huet vs. PHOAS
-- Philip Wadler, 9 Oct 2012

{-# LANGUAGE Rank2Types, GADTs #-}

module CHvsPH where

-- Two representations for lambda calculus terms are the Church
-- representation, due to Thierry Coquand and Gerard Huet, let's call it
-- CH, and PHOAS, due to Adam Chlipala, let's call it PH.  Here is a
-- Haskell program giving both encodings, and showing they are
-- interconvertible.  The CH representation is called `finally tagless'
-- by Carette, Kiselyov, and Shan, which is not the most perspicuous
-- name; Atkey, Lindley, and Yallop point out the idea goes back to
-- Coquand and Huet; PH was introduced by Chlipala.

-- Demonstrates that Coquand-Huet (CH) and PHOAS (PH) representation of
-- lambda terms are interconvertible, and that both convert to DeBruijn
-- (DB), which is used to test equality of terms.  CH and PH are typed,
-- but DB is untyped; this is because type-preserving conversion of CH
-- to DB is tricky.

-- References:

-- PHOAS

-- Adam Chlipala.
-- Parametric Higher-Order Abstract Syntax for Mechanized Semantics.
-- ICFP, September 2008.
-- http://dx.doi.org/10.1145/1411204.1411226

-- CH

-- Thierry Coquand and Gérard P. Huet 
-- Constructions: A Higher Order Proof System for Mechanizing Mathematics
-- EUROCAL '85, LNCS 203, pp 151--184, 1985
-- http://dx.doi.org/10.1007/3-540-15983-5_13

-- Jacques Carette, Oleg Kiselyov and Chung-Chieh Shan.
-- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages.
-- JFP 19(5):509--543, September 2009.
-- http://dx.doi.org/10.1017/S0956796809007205

-- Robert Atkey, Sam Lindley, and Jeremy Yallop.
-- Unembedding domain-specific languages.
-- Haskell Symposium, September 2009.
-- http://dx.doi.org/10.1145/1596638.1596644

-- DeBruijn: ExpDB

type Id = String

data ExpDB where
  VarDB :: Int -> ExpDB
  LamDB :: Id -> ExpDB -> ExpDB
  AppDB :: ExpDB -> ExpDB -> ExpDB
  deriving (Eq,Show)

-- PHOAS: ExpPH

data ExPH x a where
  VarPH :: x a -> ExPH x a
  LamPH :: Id -> (x a -> ExPH x b) -> ExPH x (a -> b)
  AppPH :: ExPH x (a -> b) -> ExPH x a -> ExPH x b

newtype ExpPH a = Hide { reveal :: forall x. ExPH x a }

-- Coquand-Huet: ExpCH

class ExCH exp where
  lamCH :: Id -> (exp a -> exp b) -> exp (a -> b)
  appCH :: exp (a -> b) -> exp a -> exp b

newtype ExpCH a = ExpCH { expCH :: forall exp. ExCH exp => exp a }

-- evalPH

newtype I a = I { unI :: a }

evalPH :: ExpPH a -> a
evalPH (Hide e)  =  h e
  where
  h :: ExPH I a -> a
  h (VarPH x)    =  unI x
  h (LamPH u f)  =  h . f . I
  h (AppPH d e)  =  h d (h e)

-- evalCH

newtype Ev a = Ev { ev :: a }

instance ExCH Ev where
  lamCH u f  =  Ev (ev . f . Ev)
  appCH d e  =  Ev (ev d (ev e))

evalCH :: ExpCH a -> a
evalCH (ExpCH e)  =  ev e

-- fromPHtoDB

newtype K a b = K { unK :: a }

fromPHtoDB :: ExpPH a -> ExpDB
fromPHtoDB (Hide e)  =  h 0 e
  where
  h :: Int -> ExPH (K Int) a -> ExpDB
  h w (VarPH v)    =  VarDB (w - unK v - 1)
  h w (LamPH u f)  =  LamDB u (h (w+1) (f (K w)))
  h w (AppPH d e)  =  AppDB (h w d) (h w e)

-- fromCHtoDB

newtype ToDB a = ToDB { toDB :: Int -> ExpDB }

instance ExCH ToDB where
  lamCH u f  =  ToDB (\w -> LamDB u (toDB (f (ToDB (\v -> VarDB (v-w-1)))) (w+1)))
  appCH d e  =  ToDB (\w -> AppDB (toDB d w) (toDB e w))

fromCHtoDB :: ExpCH a -> ExpDB
fromCHtoDB (ExpCH e)  =  toDB e 0
  

-- fromCHtoPH

instance ExCH (ExPH x) where
  lamCH u f  =  LamPH u (f . VarPH)
  appCH d e  =  AppPH d e

fromCHtoPH :: ExpCH a -> ExpPH a
fromCHtoPH (ExpCH e)  =  Hide e

-- fromPHtoCH

fromPHtoCH :: ExpPH a -> ExpCH a
fromPHtoCH (Hide e) = ExpCH (h e)
  where
  h :: ExCH exp => ExPH exp a -> exp a
  h (VarPH x)    =  x
  h (LamPH u f)  =  lamCH u (h . f)
  h (AppPH d e)  =  appCH (h d) (h e)

-- test data, PH

fourPH =
  let
    plusPH = LamPH "m" (\m -> LamPH "n" (\n -> LamPH "f" (\f -> LamPH "x" (\x ->
             VarPH m `AppPH` VarPH f `AppPH`
               (VarPH n `AppPH` VarPH f `AppPH` VarPH x)))))
    onePH  = LamPH "f" (\f -> LamPH "x" (\x -> VarPH f `AppPH` VarPH x))
    twoPH  = plusPH `AppPH` onePH `AppPH` onePH
    fourPH = plusPH `AppPH` twoPH `AppPH` twoPH
  in
    Hide fourPH

-- test data, CH

fourCH =
  ExpCH (
    let
      plusCH = lamCH "m" (\m -> lamCH "n" (\n -> lamCH "f" (\f -> lamCH "x" (\x ->
               m `appCH` f `appCH` (n `appCH` f `appCH` x)))))
      oneCH  = lamCH "f" (\f -> lamCH "x" (\x -> f `appCH` x))
      twoCH  = plusCH `appCH` oneCH `appCH` oneCH
      fourCH = plusCH `appCH` twoCH `appCH` twoCH
    in
      fourCH)


-- test

main = evalPH fourPH (+1) 0 == 4 &&
       evalCH fourCH (+1) 0 == 4 &&
       fromPHtoDB fourPH == fromPHtoDB (fromCHtoPH fourCH) &&
       fromCHtoDB fourCH == fromCHtoDB (fromPHtoCH fourPH)