9.10.12

 

CH = PH

Two representations for lambda calculus terms are the Church representation, due to Thierry Coquand (left) and Gerard Huet (middle), let's call it CH, and PHOAS, due to Adam Chlipala (right), 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.)

# posted by Philip Wadler @ 11:37 PM
Comments:
I proved that the 'CH' and 'PH' presentations are isomorphic in my TLCA2009 paper: Syntax for Free: Representing Syntax with Binding Using Parametricity, building on the well-known result that inductive types can be encoded via polymorphism in System F.
# posted by Blogger Unknown : 10/10/12 2:02 PM
 
I thought that Geoff Washburn and Stephanie Weirich proposed the PHOAS representation of lambda terms in their Boxes Go Bananas paper, and Bob gave the first proof that it was an adequate encoding?
# posted by Blogger Neel Krishnaswami : 25/10/12 11:28 AM
 
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?