Re: [Haskell] Fixpoint combinator without recursion
Edsko, (Moved to Haskell Cafe.)
It is well-known that negative datatypes can be used to encode recursion, without actually explicitly using recursion. As a little exercise, I set out to define the fixpoint combinator using negative datatypes. I think the result is kinda cool :) Comments are welcome :)
Yeah, it's rather cool. IIRC, this style of encoding of recursion operators is attributed to Morris. Before the advent of equality coercions, GHC typically had problems generating code for these kinds of definitions. Did you test this with a release version? If so, how did you get around the code- generation problem? Is it the NOINLINE pragma that does the trick? Cheers, Stefan
Yeah, it's rather cool. IIRC, this style of encoding of recursion operators is attributed to Morris.
Do you have a reference?
Before the advent of equality coercions, GHC typically had problems generating code for these kinds of definitions. Did you test this with a release version? If so, how did you get around the code- generation problem? Is it the NOINLINE pragma that does the trick?
Yep. Without the NOINLINE pragma, ghc tries to inline the definition of fac, expanding it ad infinitum (this is a known bug in ghc and mentioned in the ghc manual). Hugs doesn't have a problem though. Edsko
Edsko,
Yeah, it's rather cool. IIRC, this style of encoding of recursion operators is attributed to Morris.
Do you have a reference?
James H. Morris. Lambda calculus models of programming languages. Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of Technology, 1968. Cheers, Stefan
On Wed, Apr 04, 2007 at 11:05:51PM +0200, Stefan Holdermans wrote:
Edsko,
Yeah, it's rather cool. IIRC, this style of encoding of recursion operators is attributed to Morris.
Do you have a reference?
James H. Morris. Lambda calculus models of programming languages. Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of Technology, 1968.
Aah, I guess that's a bit old to be avaiable online :) Does he talk about negative datatypes though? The Y combinator itself isn't really the point of my little exercise; it's more that I can code the Y combinator without making any recursive calls (in fact, there aren't any recursive calls in that program at all). Edsko
Edsko,
James H. Morris. Lambda calculus models of programming languages. Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of Technology, 1968.
Aah, I guess that's a bit old to be avaiable online :) Does he talk about negative datatypes though? The Y combinator itself isn't really the point of my little exercise; it's more that I can code the Y combinator without making any recursive calls (in fact, there aren't any recursive calls in that program at all).
If I recall correctly that's exactly what he demonstrates, i.e., that fixed-point combinators can be encoded without value-level recursion, but by instead making use of types that are contravariantly recursive. Cheers, Stefan
On Wed, Apr 04, 2007 at 11:15:25PM +0200, Stefan Holdermans wrote:
Edsko,
James H. Morris. Lambda calculus models of programming languages. Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of Technology, 1968.
Aah, I guess that's a bit old to be avaiable online :) Does he talk about negative datatypes though? The Y combinator itself isn't really the point of my little exercise; it's more that I can code the Y combinator without making any recursive calls (in fact, there aren't any recursive calls in that program at all).
If I recall correctly that's exactly what he demonstrates, i.e., that fixed-point combinators can be encoded without value-level recursion, but by instead making use of types that are contravariantly recursive.
I see. Thanks for the reference! Must try to dig that up (the MIT publication database appears to be offline at the moment). Thanks again, Edsko
On Apr 4, 2007, at 5:01 PM, Edsko de Vries wrote:
Yeah, it's rather cool. IIRC, this style of encoding of recursion operators is attributed to Morris.
Do you have a reference?
Before the advent of equality coercions, GHC typically had problems generating code for these kinds of definitions. Did you test this with a release version? If so, how did you get around the code- generation problem? Is it the NOINLINE pragma that does the trick?
Yep. Without the NOINLINE pragma, ghc tries to inline the definition of fac, expanding it ad infinitum (this is a known bug in ghc and mentioned in the ghc manual). Hugs doesn't have a problem though.
I keep waiting for someone to use this fact to cook up a poor man's partial evaluation---use fix for static recursion, and ordinary recursive definitions for dynamic recursion. I fiddled with this a bit in the pH days (it had the same bug, for much the same reason). -Jan-Willem Maessen
Edsko _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Edsko de Vries -
Jan-Willem Maessen -
Stefan Holdermans