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.
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 onli
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 real
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.
> Tech
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.
C
> 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 versio
Mike,
For those of us who aren't type theorists: What's a "negative
datatype"?
A type that has a recursive call in negative position. Negative
positions are the argument positions in function types. (But if a
function type appears in a negative position, then its own argument
position i
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 wel
