-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 David House wrote:

On 31/05/07, Isaac Dupree wrote:

...

foo undefined = undefined

That's not true. When you evaluate foo undefined, it matches the first (irrefutable) pattern immediately, without any deconstruction of the undefined argument (which is the entire point of it being a lazy pattern). So it becomes the right hand side, C <thunk>. Only when you force that <thunk> would you have to force the undefined argument, so foo undefined = C undefined:

*Main> foo undefined C *** Exception: Prelude.undefined

Oh, I misinterpreted "must be non bottom" to be talking about becoming more strict, not less, compared to id, and then misanalysed the function :/ Now for the existential case... normally an existential "escaping" is useless, sometimes it seems to make sense. Looking at the GHC manual http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html... I think this is the relevant explanatory paragraph: In general, you can only pattern-match on an existentially-quantified constructor in a case expression or in the patterns of a function definition. The reason for this restriction is really an implementation one. Type-checking binding groups is already a nightmare without existentials complicating the picture. Also an existential pattern binding at the top level of a module doesn't make sense, because it's not clear how to prevent the existentially-quantified type "escaping". So for now, there's a simple-to-state restriction. We'll see how annoying it is. It seems like an existential as returned by (case y of E x -> x) is ("should" be) just "anything" -- you can put it in an existential container, or you can "seq" it, but not much else. To seq, (case y of E x -> (x `seq`)) should work, so the difficulty is in transferring an existential from one place to another with weird strictness effects... Is (data E' = forall a . E' !a) allowed? I seem to remember some discussion about its oddness... Type-class contexts on the existentials make it more complicated. Isaac -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFGYHDzHgcxvIWYTTURAn9oAJ45VLiD6W63ByUOrfpRILprPyKGdACbB+nu YIULFXH4KHDcbNmG/+cb5vI= =v2Co -----END PGP SIGNATURE-----

Ben Rudiak-Gould wrote:

It's not definable, and there is a good reason. Existential boxes in principle contain an extra field storing their hidden type, and the type language is strongly normalizing.

Thank you very much for the answer: indeed, I suspected strong normalization for types had something to do with that. More in detail, I was actually trying to understand if I could define an infinite list for the following GADT: data List len a where Nil :: List Zero a Cons :: a -> List len a -> List (Succ len) a Here, the len argument fixes the length of the list. So, if len is some fixed type - say the encoding of n - it proves that the list has length n and therefore is finite (although may contain _|_). However, I wondered if this property (finite length) might get invalidated using an existential: data AList a where L :: List len a -> AList a -- translation of: ones = 1 : ones ones :: AList Int ones = L (case ones of L os -> Cons 1 os) but the last line fails to compile. I threw anything at that, but each attempt failed. From your answer, I see that this is indeed impossible. Zun.