Is it possible to define Y in Haskell (pref' H98) -- and get it to pass type checking? -- E.g. As in SML let datatype 'a rt = recrt of ('a rt) -> 'a; fun Y G = let fun Ggg (recrt g) n = G(g (recrt g))n in Ggg (recrt Ggg) end; fun F f n = if n=0 then 1 else n*f(n-1); in Y F 3 end -- I've tried various things, some of which *seem* to put the checker in a loop? -L --
Trevion writes:
On 4/18/05, Lloyd Allison <Lloyd.Allison@infotech.monash.edu.au> wrote:
Is it possible to define Y in Haskell (pref' H98) -- and get it to pass type checking?
I believe that
y f = f (y f)
is the normal way to do it.
I've also seen this: y f = g where g = f g -- David Menendez <zednenem@psualum.com> | "In this house, we obey the laws <http://www.eyrie.org/~zednenem> | of thermodynamics!"
On Mon, 2005-04-18 at 01:08 -0400, David Menendez wrote:
Trevion writes:
On 4/18/05, Lloyd Allison <Lloyd.Allison@infotech.monash.edu.au> wrote:
Is it possible to define Y in Haskell (pref' H98) -- and get it to pass type checking?
I believe that
y f = f (y f)
is the normal way to do it.
I've also seen this:
y f = g where g = f g
Note that the second form generally gives more sharing than the first (I say generally because there is no guarantee in Haskell how much sharing you will get.) At least GHC (and probably hugs and nhc98) gives the second form a cyclic representation. See the discussion in Section 4.1 (Recursion) in "A Natural Semantics for Lazy Evaluation", John Launchbury. Bernie.
On Mon, 2005-04-18 at 15:35 +1000, Bernard Pope wrote:
On Mon, 2005-04-18 at 01:08 -0400, David Menendez wrote:
Trevion writes:
On 4/18/05, Lloyd Allison <Lloyd.Allison@infotech.monash.edu.au> wrote:
Is it possible to define Y in Haskell (pref' H98) -- and get it to pass type checking?
I believe that
y f = f (y f)
is the normal way to do it.
I've also seen this:
y f = g where g = f g
Note that the second form generally gives more sharing than the first (I say generally because there is no guarantee in Haskell how much sharing you will get.) At least GHC (and probably hugs and nhc98) gives the second form a cyclic representation.
See the discussion in Section 4.1 (Recursion) in "A Natural Semantics for Lazy Evaluation", John Launchbury.
I also meant to add that I think these solutions are not what Lloyd is after, because they rely on recursive equations, which I believe was avoided in Lloyd's SML code. Here is a translation into Haskell: --- data Rt a = Recrt (Rt a -> a) y :: (a -> a) -> a y x = ggg (Recrt ggg) where ggg (Recrt g) = x (g (Recrt g)) func :: (Int -> Int) -> Int -> Int func f n = if n==0 then 1 else n * f (n-1) main :: IO () main = print (y func 3) --- Hugs accepts this, but GHC 6.2 goes into an infinite loop on my machine. I think this is mentioned in the list of known bugs in GHC: http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html "GHC's inliner can be persuaded into non-termination using the standard way to encode recursion via a data type" Cheers, Bernie.
participants (4)
-
Bernard Pope -
David Menendez -
Lloyd Allison -
Trevion