In this function data C = C Int foo :: C -> C foo ~(C x) = C x foo is _not_ the identity: its result must be non bottom, i.e. the constructor C is "forced" to its argument. I wonder if a similar function is definable for existential types: data E = forall a . E a foo :: E -> E foo, as defined above does not work (lazy patterns not allowed), and in foo y = E (case y of E x -> x) a variable escapes. I also tried with CPS with no success. Is foo definable at all? I'm starting to think that it is not, and that there must be a very good reason for that... Thank you, Zun.
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Roberto Zunino wrote:
In this function
data C = C Int foo :: C -> C foo ~(C x) = C x
foo is _not_ the identity: its result must be non bottom, i.e. the constructor C is "forced" to its argument.
foo undefined = undefined foo (C undefined) = C undefined foo (C 13) = C 13 Looks like the identity to me? (id _is_ strict after all) foo' (C x) = x `seq` (C x) would be different though: foo' (C undefined) = undefined Isaac -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFGX0HQHgcxvIWYTTURAoE2AKDFNn2bSVqoVjqWj8jyBfgKjYVh1gCeLqdT pGz49AfTUbblaMeeyBR8a84= =sFp6 -----END PGP SIGNATURE-----
On 31/05/07, Isaac Dupree <isaacdupree@charter.net> 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 -- -David House, dmhouse@gmail.com
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 David House wrote:
On 31/05/07, Isaac Dupree <isaacdupree@charter.net> 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-----
Roberto Zunino wrote:
foo, as defined above does not work (lazy patterns not allowed), and in
foo y = E (case y of E x -> x)
a variable escapes. I also tried with CPS with no success.
Is foo definable at all? I'm starting to think that it is not, and that there must be a very good reason for that...
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. If you make the type argument explicit, you have foo (E <t> x) = E <t> x foo _|_ = E ??? _|_ The ??? can't be a divergent type term, because there aren't any; it must be a type, but no suitable type is available (foo has no type argument). You can't even use some default dummy type like (), even though _|_ does have that type, because you'd have to solve the halting problem to tell when it's safe to default. I'm less clear on how important it is that type terms don't diverge. I think it may be possible to write cast :: a -> b if this restriction is removed, but I don't actually know how to do it. -- Ben
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.
participants (4)
-
Ben Rudiak-Gould -
David House -
Isaac Dupree -
Roberto Zunino