-- 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)