Hello, how do I unbox a existential quantificated data type?
{-# LANGUAGE ExistentialQuantification #-} data L a = forall l. L (l a) unboxL (L l) = l
is giving me, in GHC: Inferred type is less polymorphic than expected Quantified type variable `l' escapes When checking an existential match that binds l :: l t The pattern(s) have type(s): L t The body has type: l t In the definition of `unboxL': unboxL (L l) = l Thanks. -- Marco Túlio Gontijo e Silva Página: http://marcotmarcot.googlepages.com/ Blog: http://marcotmarcot.blogspot.com/ Correio: marcot@riseup.net XMPP: marcot@jabber.org IRC: marcot@irc.freenode.net Telefone: 25151920 Celular: 98116720 Endereço: Rua Turfa, 639/701 Prado 30410-370 Belo Horizonte/MG Brasil
On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
Hello,
how do I unbox a existential quantificated data type?
You can't. You have to use case analysis: case foo of L l -> <whatever you wanted to do> where none of the information your case analysis discovers about the actual type of l can be made available outside of the scope of the case expression. (It can't `escape'). This is required for decidable static typing, IIRC. jcc
{-# LANGUAGE ExistentialQuantification #-} data L a = forall l. L (l a) unboxL (L l) = l
is giving me, in GHC:
Inferred type is less polymorphic than expected Quantified type variable `l' escapes When checking an existential match that binds l :: l t The pattern(s) have type(s): L t The body has type: l t In the definition of `unboxL': unboxL (L l) = l
Thanks.
On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
Hello,
how do I unbox a existential quantificated data type?
You can't. You have to use case analysis:
case foo of L l -> <whatever you wanted to do>
where none of the information your case analysis discovers about the actual type of l can be made available outside of the scope of the case expression. (It can't `escape'). This is required for decidable static typing, IIRC.
It's not an extraneous requirement; it is part of the definition of existential types.
On Sun, 2008-07-13 at 18:28 -0500, Derek Elkins wrote:
On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
Hello,
how do I unbox a existential quantificated data type?
You can't. You have to use case analysis:
case foo of L l -> <whatever you wanted to do>
where none of the information your case analysis discovers about the actual type of l can be made available outside of the scope of the case expression. (It can't `escape'). This is required for decidable static typing, IIRC.
It's not an extraneous requirement; it is part of the definition of existential types.
I know that. I didn't know implementing existential types was an end in itself, though. jcc
On 2008 Jul 13, at 19:50, Jonathan Cast wrote:
On Sun, 2008-07-13 at 18:28 -0500, Derek Elkins wrote:
On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
Hello,
how do I unbox a existential quantificated data type?
You can't. You have to use case analysis:
case foo of L l -> <whatever you wanted to do>
where none of the information your case analysis discovers about the actual type of l can be made available outside of the scope of the case expression. (It can't `escape'). This is required for decidable static typing, IIRC.
It's not an extraneous requirement; it is part of the definition of existential types.
I know that. I didn't know implementing existential types was an end in itself, though.
No? Consider ST. Anytime you need to completely restrict access to the innards of a datum, existential types are your friend. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
On Sun, 2008-07-13 at 21:03 -0400, Brandon S. Allbery KF8NH wrote:
On 2008 Jul 13, at 19:50, Jonathan Cast wrote:
On Sun, 2008-07-13 at 18:28 -0500, Derek Elkins wrote:
On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
Hello,
how do I unbox a existential quantificated data type?
You can't. You have to use case analysis:
case foo of L l -> <whatever you wanted to do>
where none of the information your case analysis discovers about the actual type of l can be made available outside of the scope of the case expression. (It can't `escape'). This is required for decidable static typing, IIRC.
It's not an extraneous requirement; it is part of the definition of existential types.
I know that. I didn't know implementing existential types was an end in itself, though.
No? Consider ST. Anytime you need to completely restrict access to the innards of a datum, existential types are your friend.
Right. Mea culpa. jcc
On Thursday 10 July 2008, Marco Túlio Gontijo e Silva wrote:
Hello,
how do I unbox a existential quantificated data type?
{-# LANGUAGE ExistentialQuantification #-} data L a = forall l. L (l a) unboxL (L l) = l
is giving me, in GHC:
Inferred type is less polymorphic than expected Quantified type variable `l' escapes When checking an existential match that binds l :: l t The pattern(s) have type(s): L t The body has type: l t In the definition of `unboxL': unboxL (L l) = l
You don't. Or, at least, you don't do it that way. The point of an existential is that the quantified type is 'forgotten', and there's no way to get it back. That's good for abstraction, in that it restricts you to using some provided interface that's guaranteed to work with the forgotten type, but it means that you can't just take things out of the existential box. Instead, you have to use them in ways that make the forgotten type irrelevant (that is, ways that are parametric in the corresponding type). The type of the unboxL function in a type system with first-class existentials is something like: unboxL :: L a -> (exists l. l a) Of course, GHC doesn't do first-class existentials, otherwise you'd probably not be bothering with the datatype in the first place. :) The proper way to eliminate an existential is (as mentioned above) with a universal: elim :: (exists l. l a) -> (forall l. l a -> r) -> r elim e f = f e Or, since existentials in GHC are restricted to data types: elim :: L a -> (forall l. l a -> r) -> r elim (L e) f = f e Of course, as has already been noted, elim foo (\l -> stuff) is equivalent to: case foo of L l -> stuff and doesn't need rank-2 polymorphism enabled, to boot. :) -- Dan
On Thu, 10 July 2008, Marco Túlio Gontijo e Silva wrote:
how do I unbox a existential quantificated data type?
Dan Doel wrote:
elim :: L a -> (forall l. l a -> r) -> r elim (L e) f = f e
Just one catch: You can't actually write a function 'f' of type (forall l. l a -> r) without knowing something about the forgotten type of l. One way to deal with this is by restricting the type of l in the data declaration. For example, you could restrict it to the typeclass Foldable, and then you have access to the methods of that typeclass. \begin{code} {-# LANGUAGE ExistentialQuantification #-} module Main where import qualified Data.Foldable as F data L a = forall l. (F.Foldable l) => L (l a) toList :: L a -> [a] toList (L x) = F.foldr (:) [] x main :: IO () main = do let x = L [1..10] print $ toList x \end{code} See also http://www.haskell.org/haskellwiki/Existential_type
participants (6)
-
Brandon S. Allbery KF8NH -
Dan Doel -
Derek Elkins -
Jonathan Cast -
Marco Túlio Gontijo e Silva -
Ronald Guida