Lemma: Assuming eta-equivalence we have that (\x -> ⊥) = ⊥ :: A -> B.

Proof: ⊥ = (\x -> ⊥ x) by eta-equivalence, and (\x -> ⊥ x) = (\x -> ⊥) by reduction under the lambda.

The Haskell 2010 report, section 6.2 specifies the seq function by two equations:

seq :: a -> b -> b
seq ⊥ b  =  ⊥
seq a b  =  b, if a ≠ ⊥

It then claims "As a consequence, ⊥ is not the same as \x -> ⊥, since seq can be used to distinguish them."

My question is, is that really a consequence of the definition of seq?

The implicit argument seems to be that seq would be uncomputable if seq (\x -> ⊥) b = ⊥. However I haven't been able to prove that such a seq would be uncomputable. It seems to me such a seq is both monotone, and continuous, which puts it in the the realm of being computable.

An algorithm that implement such as seq might work by attempting to search for for some x where f x ≠ ⊥ by enumerating the domain of f starting with ⊥. Though such an implementation, even if possible at all, gets pretty hairy once we want to make seq polymorphic.

Is there a proof that there is no computable seq that identifies (\x -> ⊥) with ⊥ :: A -> B? Alternatively, is there some construction of seq that does identify (\x -> ⊥) with ⊥ :: A -> B?

First, let us be explicit about how seq distinguishes $\bot$ from $\lambda x . \bot$:

bottom :: a
bottom = bottom

eta :: a -> b
eta x = bottom

-- This terminates
fortytwo = seq eta 42

-- This does not terminate
infinity = seq bottom 42

It is therefore an experimental fact that in Haskell $\bot$ and $\lambda x . \bot$ are operationally distinguishable. It is also a fact, and a quite obvious one, that seq is computable because Haskell computes it. So much about Haskell. You are asking about the very particular phrasing of the Haskell documentation. I read it as saying that seq is supposed to satisfy the two given equations, but those two equations are not sufficient for the definition of seq. Here is why: I can give you two models of (simply typed) $\lambda$-calculus in which seq is computable and satisfies the given equations, but in one of the models $\bot$ and $\lambda x . \bot$ agree, while in the other they do not.

In a simple domain-theoretic model where $\lambda$-expressions are interpreted in the domain of continuous functions $[D \to E]$ we have $\bot = \lambda x . \bot$, obviously. Take effective Scott domains or some such to make everything computable. It is easy to define seq in such a model.

We can also have a model of $\lambda$-calculus in which seq distinguishes $\bot$ and $\lambda x . \bot$, and then of course $\eta$-rule cannot hold. For instance, we can do this by interpreting functions in the domain $[D \to E]_\bot$, i.e., the function space domain with an extra bottom attached. Now $\bot$ is, well, the bottom of $[D \to E]_\bot$, while $\lambda x . \bot$ is the element just above it. They cannot be distinguished by application because they both evaluate to $\bot$, no matter what you apply them to (they are extensionally equal). But we do have seq as a map between domains and it alwyas distinguishes bottom from all other elements.

  • 1
    It is an experimental fact that in GHC and/or Hugs ⊥ and λx.⊥. Fortunately, Haskell isn't defined by an implementation. My question is suggesting that Haskell is underspecified with regards to seq. – Russell O'Connor Oct 1 '13 at 22:50
  • Can you give a reference to what you mean by "effective Scott domains" Presumably that doesn't imply that the partial order is decidable. Also, the STLC isn't polymorphic, but Haskell is. Usually Haskell is interpreted in System F or one of its derivatives. How does this affect your argument? – Russell O'Connor Oct 1 '13 at 22:55
  • Section 1.1.4 of my Ph.D. dissertation andrej.com/thesis/thesis.pdf has a short definition of effective Scott domains, and this is actually the first Google hit that is freely available. – Andrej Bauer Oct 2 '13 at 14:16
  • 2
    If you write a proof for me you will get an implementation of Haskell 98 where the eta-rule holds allowing (foldr (\a b -> f a b) z xs) to be optimized to (foldr f z xs) causing an asymptotic performance increase from O(n^2) to O(n) (see ghc.haskell.org/trac/ghc/ticket/7436). More compelling it will allow a NewTypeWrapper in (NewTypeWrapper . f) to be optimized away without forcing f to be eta-expanded and prevent some asymptotic performance penalties currently imposed by newTypes in GHC (in the use of foldr for example). – Russell O'Connor Oct 2 '13 at 17:08
  • 1
    Actually, you would have to make sure that your compiler always implements $\lambda x . \bot$ as $\bot$. That is, you might be tempted to not always contract and so in principle $\lambda x . \bot$ and $\bot$ would be "sometimes distinguishable", a very dangerous situation. To make sure this is not the case, you need to implement seq in a clever way which involves spawning infinitely many processes each applying your function to a basic element. If any of the processes terminates, then seq may proceed. It would be interesting to see if we can do this sequentially. Hmm. – Andrej Bauer Oct 3 '13 at 0:13

Note that the specification for seq which you quote is not its definition. To quote the Haskell report "The function seq is defined by the equations: [and then the equations you give]".

The suggested argument seems to be that seq would be uncomputable if seq (\x -> ⊥) b = ⊥.

Such behaviour would violate the specification of seq.

Importantly, since seq is polymorphic, seq cannot be defined in terms of deconstructors (projections/pattern matching, etc.) on either of the two parameters.

Is there a proof that there is no computable seq that identifies (\x -> ⊥) with ⊥ :: A -> B?

If seq' (\x -> ⊥) b, one might think we could apply the first parameter (which is a function) to some value and then get ⊥ out. But, seq can never identify the first parameter with a function value (even if it happens to be one for some use of seq) because of its parametric polymorphic type. Parametricity means we know nothing about the parameters. Furthermore, seq can never take an expression and decide "is this ⊥?" (cf. the Halting problem), seq can only try to evaluate it, and itself diverge to ⊥.

What seq does is to evaluate the first parameter (not fully, but to "weak head normal form" [1], i.e. to the top-most constructor), then return the second parameter. If the first parameter happens to be (i.e., a non terminating computation) then evaluating it causes seq to non-terminate, and thus seq ⊥ a = ⊥.

[1] Free Theorems in the Presence of seq - Johann, Voigtlander http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf

  • The specification I give for seq is the definition of seq because that is exactly what the Haskell 2010 report says in Section 6.2. Your operation definition of seq is not supported by the Haskell 2010 report: the words "head normal form" only occur once in the report in a totally different context. It also is inconsistent with my understanding that GHC will often reduce the second argument to seq before the first argument, or the first argument won't be reduced at all because the strictness analyzer has proved it is non-bottom statically. – Russell O'Connor Sep 27 '13 at 22:03
  • Parametricity doesn't directly say that we cannot apply any deconstructors, nor does it say we can never identify the first parameter with a function value. All parametercity says for the polymorphic lambda calculus with fixpoints is that seq can absorb strict functions, or more generally certain strict relations hold for terms contain seq. I admit it is plausible that parametricity might be used to prove (\x -> ⊥) ≠ ⊥, but I would like to see a rigorous proof. – Russell O'Connor Sep 27 '13 at 22:09
  • In the case of a function f : forall a . a -> T (where T is some other type), then f cannot apply any deconstructors to its first argument since it does not know which deconstructors to apply. We cannot do a "case" on types. I have tried to improve the above answer (including citing information on seq evaluating to head normal form). – dorchard Sep 28 '13 at 12:31
  • I can try to do the rigorous proof later if I find time (using relations in the style of Reynolds might be a good approach). – dorchard Sep 28 '13 at 12:32
  • @RussellO'Connor: the description of seq is not "inconsistent" with those behaviors, it's just an operational specification (and behaviors are optimizations which do not change the final result). – Blaisorblade Mar 24 '14 at 16:27

I am not sure if the Haskell report defines the semantics rigorously enough to settle the question about what $\lambda x.\, \bot$ should mean. However, it is common experience in Haskell as well as all other lazy functional languages, that, if you ask them to evaluate a term that represents $\lambda x.\, \bot$, the evaluation terminates. The "As a consequence..." remark in the Haskell report is assuming that the reader knows this.

Samson Abramsky considered this issue a long time ago and wrote a paper called "The Lazy Lambda Calculus". So, if you want formal definitions, this is where you might look.

  • 1
    Apparently, these details are only defined by desugaring into the "Haskell kernel". Where is it defined is it? The report says, in Sec. 1.2: "Although the kernel is not formally specified, it is essentially a slightly sugared variant of the lambda calculus with a straightforward denotational semantics. The translation of each syntactic structure into the kernel is given as the syntax is introduced." – Blaisorblade Mar 24 '14 at 16:30
  • The Haskell 2010 report says the same, amazingly. – Blaisorblade Mar 24 '14 at 16:52
  • Thanks for the reference to Abramsky! I skimmed it to see how it answers the question, and I came up with the following answer: cstheory.stackexchange.com/a/21732/989 – Blaisorblade Mar 24 '14 at 17:55

Proving that λ x. Ω ‌≠ Ω in is one of the goals Abramsky sets for his lazy lambda calculus theory (page 2 of his paper, already cited by Uday Reddy), because they are both in weak head normal form. As of definition 2.7, he discusses explicitly that eta-reduction λ x. M x → M is not generally valid, but it is possible if M terminates in every environment. This does not mean that M must be a total function — only that evaluating M must terminate (by reducing to a lambda, for instance).

Your question seems to be motivated by practical concerns (performance). However, even though the Haskell Report might be less than completely clear, I doubt that equating λ x. ⊥ ‌with ⊥ would produce a useful implementation of Haskell; whether it implements Haskell '98 or not is debatable, but given the remark, it's clear that the authors intended it to be the case.

Finally, how's seq to generate elements for an arbitrary input type? (I know QuickCheck defines the Arbitrary typeclass for that, but you're not allowed to add such constraints here). This violates parametricity.

Updated: I didn't manage to code this right (because I'm not so fluent in Haskel), and fixing this seems to require nested runST regions. I tried using a single reference cell (in the ST monad) to save such arbitrary elements, read them later, and make them universally available. Parametricity proves that break_parametricity below cannot be defined (except by returning bottom, e.g. an error), while it could recover the elements your proposed seq would generate.

import Control.Monad.ST
import Data.STRef
import Data.Maybe

produce_maybe_a :: Maybe a
produce_maybe_a = runST $ do { cell <- newSTRef Nothing; (\x -> writeSTRef cell (Just x) >> return x) `seq` (readSTRef cell) }

break_parametricity :: a
break_parametricity = fromJust produce_maybe_a

I have to admit that I'm slightly fuzzy on formalizing the parametricity proof needed here, but this informal use of parametricity is standard in Haskell; but I learned from Derek Dreyer's writings that the needed theory is being quickly worked out in these last years.

EDITs:

  • I am not even sure whether you need those extensions, which are studied for ML-like, imperative and untyped languages, or whether the classical theories of parametricity cover Haskell.
  • Also, I mentioned Derek Dreyer simply because I only later came across Uday Reddy's work — I learned about it only recently from "The essence of Reynolds". (I only started really reading literature on parametricity in the last month or so).
  • Evaluating (\x -> writeSTRef cell (Just x) >> return x) on random inputs does not execute a write to the cell. Only the ST commands that make it into the sequenced passed into runST are ever executed. Similarly, running main = (putStrLn "Hello") `seq` (return ()) does not print anything onto the display. – Russell O'Connor Apr 6 '14 at 5:36
  • @RussellO'Connor, of course you're right — testing is hard since seq does not have the behavior we discuss. But I still think generating elements breaks parametricity per se. I'll try fixing the answer to exemplify that. – Blaisorblade Apr 7 '14 at 10:18
  • Hm, the obvious fix to the answer requires nesting runST regions and using the cell from the outer region in the inner one, but that's not allowed. – Blaisorblade Apr 7 '14 at 19:37

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.