Re: [Haskell-cafe] Type-indexed expressions with fixpoint

oleg@okmij.org wrote:

Brent Yorgey wrote:

John Reynolds showed long ago that any higher-order language can be encoded in first-order. We witness this every day: higher-order language like Haskell is encoded in first-order language (machine code). The trick is just to add a layer of interpretive overhead -- I mean, a layer of interpretation. The closure conversion on type level was shown in http://okmij.org/ftp/Computation/lambda-calc.html#haskell-type-level

Brent, Do you have the reference for Reynolds higher-order to first-order encoding. Regards, Pat