Comments on: Searching Infinity Parametrically

By: Ryan Ingram

Ryan Ingram — Wed, 22 Feb 2012 23:43:08 +0000

Hm, I changed my mind. effectify requires you to order all the calls inside the otherwise pure f, which violates referential transparency; in (\k :: (String->Int) -> k “a” + k “b”) (with strict (+)), the compiler is allowed to choose whether it wants to evaluate k “a” or k “b” first, while in the effectful version the caller needs to explicitly make that decision.

By: Ryan Ingram

Ryan Ingram — Wed, 22 Feb 2012 23:02:20 +0000

One thing that’s interesting to me is the transformation from

type Pure a b c = (a -> b) -> c

type Effect a b c = forall f. Monad f => (a -> f b) -> f c

Clearly f_effect is pure; you can get f_pure from f_effect by specializing f to the identity monad:

purify :: Effect a b c -> Pure a b c
purify f ab = runIdentity $ f $ \a -> Identity $ ab a

But it seems to me that no unsoundness is introduced by allowing this isomorphism in the other direction as well, although I don’t think that’s implementable in Haskell.

effectify :: Pure a b c -> Effect a b c
effectify f = ???

By: Edward Kmett

Edward Kmett — Sun, 25 Dec 2011 20:22:35 +0000

Sean: the fact that we can search it in finite time derives from the fact that the predicate is required to evaluate in a bounded amount of time regardless of the ’size’ of the input. This keeps me from trying to compare with a lazy nat with infinity, and ensures I only look at so many of the results from the Cantor space.

The ability to do this in finite time would hold even if you had a language that could represent uncountably many programs! That I believe was Andrej’s point.

Consider data vs. codata. Think of the Cantor’s space as ‘codata’. It is infinitely large, but we can productively consume any finite portion of it. Determining the neighborhood used by a predicate only requires a finite amount of time, and then we wrap back into codata by filling in the infinite set of other cases with a valid inhabitant.

Ultimately all we have to do is find the neighborhood that was inspected (which is finite and can be done in finite time) and find a member of that neighborhood where the property does or does not hold.

This ability to search doesn’t make any use of the finiteness of the language. The finiteness of the language is interesting but irrelevant for this purpose.

By: Dan Doel

Dan Doel — Sun, 25 Dec 2011 20:14:11 +0000

“Are you saying there are only countably many streams of bits in the real world?”

What would make you think there are even infinitely many streams of bits in the real world?

By: Sean

Sean — Sun, 25 Dec 2011 18:40:40 +0000

> With that we jump clear from countable infinity to uncountable infinity, but it can still be searched in finite time!

Indeed, when we take uncountable to mean subcountable, I find it far less shocking that we can search it in finite time. To propose that we can search an uncountable ZFC set in finite time is a much stranger proposition.

By: Sean

Sean — Sun, 25 Dec 2011 18:18:57 +0000

@Dan P: I don’t see what any of this has to do with implementation details of any form. I’m just requiring some bijection between integers and strings which we interpret as Haskell code (Godel numbering will do).

@Andrej: Agreed (although I don’t believe I’m requiring any sort of quoting mechanism…). I’m simply arguing that while “uncountable” has the same formal definition, intuitively it behaves much differently than it does in ZFC. In ZFC it means “very large”, while in this kind of intuitionistic setting it can mean “smaller than countable” (subcountable). The meanings are so different that I’m leery to call them the same thing, for fear that we mislead the classical mathematicians.

By: Andrej Bauer

Andrej Bauer — Sun, 25 Dec 2011 14:08:52 +0000

@Sean: the definition of countable simply is “there is a surjection from the natural numbers”. Subsets of countable sets are called “subcountable” and can be very, very complicated in intuitionistic logic, for example they need not be countable. In addition, your proposed plan to take codes of functions does not quite work inside Haskell, as there is no way to get the code of a function in Haskell, i.e., all total maps (int -> bool) -> int are constant. You would have to extend Haskell by some sort of a quoting mechanism that would allow you to always access source code (or the machine instructions of the compiled code). With such modifications your idea demonstrates the fact that it is consistent to assume intuitionistically that the Cantor space is a quotient of a subset of a countable set. Nevertheless, it is still uncountable.

By: Dan P

Dan P — Sun, 25 Dec 2011 10:22:47 +0000

@Sean: one of the nice things about Haskell is that you can pretty much run it on paper or on an abstract machine.

We use it to model mathematical ideas all the time, ignoring the fact that (for example) Integer, being implemented on top of GMP, is finite (2^53 bits or something is the maximum allowed, even if you did have infinite memory). I think that pointing out one of the implementation details of one of Haskell’s “interpreters” (a CPU) is kind of missing the point here.

By: Sean

Sean — Sun, 25 Dec 2011 08:25:02 +0000

@Andrej: Fair enough, but if you want to stay within Haskell, your definition of “uncountable” may not be what you are expecting anymore. It’s true that there is no total surjection e : Integer -> (Integer -> Bool), but there is a partial surjection. Decode the Integer into Haskell code via your favorite encoding, and interpret the Haskell code. Some will fail to decode as well-typed Haskell programs of type Integer -> Bool, and some will fail to terminate. But you’ll cover all of them. So in some sense there are actually “fewer” functions Integer -> Bool than there are Integers.

As for the existence of uncountably many streams of bits in the real world, I’m not willing to make any sort of commitment on that statement. I will say that no one has yet satisfactorily shown me uncountably many streams in the real world :)

By: Andrej Bauer

Andrej Bauer — Sun, 25 Dec 2011 07:52:56 +0000

@Sean: It is not fair to judge a Haskell type from outside Haskell. As far as Haskell is concerned, Integer -> Bool is uncountable. Given any sequence alleged enumeration e : Integer -> (Integer -> Bool) of cantor space, the sequence \n -> not (e n n) is missed by e. So you cannot enumerate the type in Haskell, which is the relevant thing, who cares if god can enumerate Haskell types? (Yes, it takes the birth of Jesus to enumerate total functions, so Merry Christmas!) And another observation: Haskell has access to the real world and can use real-world data to construct elements of type Integer -> Bool. Are you saying there are only countably many streams of bits in the real world?

@Edward: Very nice post. I suspected something of the kind can be done, but you’re very good at minimizing the “damage” done by explicit monads. One questions remains, I think. What specification is the input predicate supposed to satisfy? The LICS 2010 paper by Martin Hofmann et al. might be relevant, see http://www2.in.tum.de/bib/files/Hofmann10Pure.pdf. They also use the trick with “parametric in all monads”.