On Wed, Apr 04, 2007 at 07:39:24PM +0100, Edsko de Vries wrote:
> Hey,
>
> 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 :)
>
> module Y where
>
> {-# NOINLINE app #-}
>
> data Fn a = Fn (Fn a -> Fn a) | Value a
> -- Application
> app :: Fn a -> Fn a -> Fn a
> app (Fn f) x = f x
>
> -- \x -> f (x x)
> delta :: Fn a -> Fn a
> delta f = Fn (\x -> f `app` (x `app` x))
>
> -- Y combinator: \f -> (\x -> f (x x)) (\x -> f (x x))
> y :: Fn a -> Fn a
> y f = delta f `app` delta f
>
> -- Lifting a function to Fn
> lift :: (a -> a) -> Fn a
> lift f = Fn (\(Value x) -> Value (f x))
>
> -- Inverse of lift
> unlift :: Fn a -> (a -> a)
> unlift f = \x -> case f `app` Value x of Value y -> y
>
> -- Fixpoint combinator
> fix :: ((a -> a) -> (a -> a)) -> (a -> a)
> fix f = unlift (y (Fn (\rec -> lift (f (unlift rec)))))
>
> -- Example: factorial
> facR f n = if n == 1 then 1 else n * f (n - 1)
> fac = fix facR
This isn't just a negative datatype, it embeds the typeless lambda calculus!
A stronger-ly typed solution:
newtype Curry o = Curry { unCurry :: Curry o -> o }
-- Curry's paradoxical type - (((...) -> o) -> o) -> o).
-- or as wikipedia puts it, If this statement is true, then O
lemma :: Curry o -> o
lemma co@(Curry f) = f co
-- Curry ANYTHING is true
mkcurry :: Curry o
mkcurry = Curry lemma
myFix :: (o -> o) -> o
myFix = lemma mkcurry
Fixing the operational semantics is left as an excersise for the reader :)
(btw, when was it first noticed that church's Omega corresponds to
Curry's paradox?)
Stefan
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
