[Haskell-cafe] Type-indexed expressions with fixpoint
pbrowne
Patrick.Browne at comp.dit.ie
Sat Nov 14 14:07:25 EST 2009
oleg at 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
More information about the Haskell-Cafe
mailing list