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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
