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

2009-11-14 Thread pbrowne
o...@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

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

2009-11-14 Thread Pierre-Evariste Dagand
Do you have the reference for Reynolds higher-order to first-order encoding. The reference discussed here is very likely to be: Definitional Interpreters for Higher-Order Programming Languages http://www.brics.dk/~hosc/local/HOSC-11-4-pp363-397.pdf You might also be interested in:

[Haskell-cafe] Type-indexed expressions with fixpoint

2009-11-10 Thread oleg
Brent Yorgey wrote: This email is literate Haskell. I'm struggling to come up with the right way to add a fixpoint constructor to an expression language described by a type-indexed GADT (details below). but since Haskell doesn't have type-level lambdas, I don't see how to make that work.

[Haskell-cafe] Type-indexed expressions with fixpoint

2009-11-09 Thread Brent Yorgey
Hi all, This email is literate Haskell. I'm struggling to come up with the right way to add a fixpoint constructor to an expression language described by a type-indexed GADT (details below). Any suggestions, comments, or pointers welcome. {-# LANGUAGE KindSignatures, GADTs #-} Consider the