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