Fixpoint combinator without recursion
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 :) Edsko {- Definition of the fixpoint combinator without using recursion Thanks to Dimitri Vytiniotis for an explanation of the basic principle. -} 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
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
For those of us who aren't type theorists: What's a "negative datatype"? Mike 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 :)
Edsko
{- Definition of the fixpoint combinator without using recursion Thanks to Dimitri Vytiniotis for an explanation of the basic principle. -}
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 _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
On Wed, Apr 04, 2007 at 01:36:18PM -0700, Michael Vanier wrote:
For those of us who aren't type theorists: What's a "negative datatype"?
Negative isn't the usual term; we mostly call them 'contravariantly recursive' data types, due to CT influence. Anyways the thing to note is that the value appears recursively, on the left of an arrow. data Foo = Foo (Foo -> Bool) -- contravariantly recursive data Foo = Foo (Bool -> Foo) -- covariantly recursive Stefan
What is it called if it's both? Is this even legal in Haskell? It seems as though this would not be a grounded type, going on forever in both directions. Dan Stefan O'Rear wrote:
On Wed, Apr 04, 2007 at 01:36:18PM -0700, Michael Vanier wrote:
For those of us who aren't type theorists: What's a "negative datatype"?
Negative isn't the usual term; we mostly call them 'contravariantly recursive' data types, due to CT influence. Anyways the thing to note is that the value appears recursively, on the left of an arrow.
data Foo = Foo (Foo -> Bool) -- contravariantly recursive data Foo = Foo (Bool -> Foo) -- covariantly recursive
Stefan _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
On Wed, Apr 04, 2007 at 02:57:06PM -0700, Dan Weston wrote:
What is it called if it's both? Is this even legal in Haskell? It seems as though this would not be a grounded type, going on forever in both directions.
I guess "negative datatype" is being a bit loose with terminology; the function constructor (->) has a negative (also called contravariant) and a positive (covariant) argument; I used "negative datatype" to mean a datatype that has a negative occurence of the data type being defined. It is perfectly valid Haskell and can be quite useful, for instance to define streams, or higher order abstract syntax (HOAS) - but it does have some strange properties, not the least of which is that it gives you recursion :) For that reason, Coq for example forbids negative occurences (because all functions must terminate); this is known as the positivity condition. I don't know which terminology (positive/negative, contravariant/covariant) is more common; I guess it depends on the community. Note that even in a definition where the type being defined is used in both the negative and the positive location, there are perfectly valid and terminating terms of that type: data Foo = Foo (Foo -> Foo ) Here is an instance of Foo: Foo id Edsko
Dan Weston wrote:
What is it called if it's both?
Then we say "the argument occurs in both positive and negative positions" or "the argument occurs in both covariant and contravariant positions". There doesn't seem to be a shorter name. I want to note that this kind of thing drives OOP crazy.
On 4/5/07, Albert Y. C. Lai <trebla@vex.net> wrote:
Dan Weston wrote:
What is it called if it's both?
Then we say "the argument occurs in both positive and negative positions" or "the argument occurs in both covariant and contravariant positions". There doesn't seem to be a shorter name. I want to note that this kind of thing drives OOP crazy.
I know that types like
data T = T (T -> T)
are inhabitated by things other than bottom (like id or \_ -> undefined), but can it be useful for *anything*? Cheers, -- Felipe.
On Thu, Apr 05, 2007 at 06:26:17PM -0300, Felipe Almeida Lessa wrote:
I know that types like
data T = T (T -> T)
are inhabitated by things other than bottom (like id or \_ -> undefined), but can it be useful for *anything*?
Yes. In particular, types like those can produce an explicit embedding of general recursion. There is a world of difference between not having a proof of strong normalization, and having a proof that strong normalization does not hold. If you don't like theory, then I'll say that you can use types like those to embed typeless lambda calculi in Haskell. Stefan
Then we say "the argument occurs in both positive and negative positions" or "the argument occurs in both covariant and contravariant positions". There doesn't seem to be a shorter name. I want to note that this kind of thing drives OOP crazy.
i recall this paper being of some help:-) http://citeseer.ist.psu.edu/castagna94covariance.html Covariance and Contravariance: Conflict without a Cause (1994) Giuseppe Castagna ACM Transactions on Programming Languages and Systems
I know that types like
data T = T (T -> T)
are inhabitated by things other than bottom (like id or \_ -> undefined), but can it be useful for *anything*?
you are in good company with that kind of question. have a look at Dana Scott's Turing Award paper for some personal notes on how he set out to show Christopher Strachey "that he was all wrong.. it [lambda-calculus] was a formal device.. it had no mathematical basis.. I had actually convinced him by 'superior logic' to give up the type-free lambda-calculus", followed by "once the doubt .. was there, it was not long before I had found one of the spaces isomorphic with its own function space, which provides a model of the 'type-free' lambda-calculus". http://awards.acm.org/citation.cfm?id=3562254&srt=all&aw=140&ao=AMTURING claus
participants (7)
-
Albert Y. C. Lai -
Claus Reinke -
Dan Weston -
Edsko de Vries -
Felipe Almeida Lessa -
Michael Vanier -
Stefan O'Rear