[Haskell-cafe] How to bring existentially quantified type variables into scope

[Wolfgang Jeltsch]

Hi!
I must say that I do not really understand this, but I nevertheless
doubt that it solves my problem. In your code, you are already starting
with the value IsListType whose type you specify as [a]. In this case,
there is nothing to find out about the element type; you already know
that it is a. My situation is that I have some type l and a value p ::
IsListType l. A successful match of p against the pattern IsListType
tells me that there is an a with l ~ [a]. However, I cannot refer to
this a.
All the best,
Wolfgang
Am Donnerstag, den 10.08.2017, 16:35 -0700 schrieb Michael Burge:
> Could something like this work for you? Here, a ~ b and you have
> access to b:
> 
> case (IsListType :: IsListType [a], Proxy :: Proxy a) of
>     (_, proxy :: Proxy b) -> asProxyTypeOf undefined proxy :: b
> 
> On Thu, Aug 10, 2017 at 4:16 PM, Wolfgang Jeltsch 
> .info> wrote:
> > Hi!
> > 
> > GHC has some support for referring to existentially quantified type
> > variables. For example, consider the following definition:
> > 
> > > data SomeList = forall a . SomeList [a]
> > 
> > With the ScopedTypeVariables extension, you can get hold of the
> > concrete
> > type a used in a SomeList value:
> > 
> > > f :: SomeList -> SomeList
> > > f (SomeList [x :: a]) = SomeList xs where
> > >
> > >     xs :: [a]
> > >     xs = [x, x]
> > 
> > However, this approach does not work if there are no fields whose
> > type
> > involves the existentially quantified type variable. Consider, for
> > example, the following definition:
> > 
> > > data IsListType a where
> > >
> > >     IsListType :: IsListType [b]
> > 
> > For each type T, we can match a value of type IsListType T against
> > the
> > pattern IsListType. If this succeeds, we know that T is a list type,
> > but
> > we do not have access to the respective element type.
> > 
> > Is there a way to determine existentially quantified type variables
> > like
> > the b in the above example?
> > 
> > All the best,
> > Wolfgang
> > _______________________________________________
> > Haskell-Cafe mailing list
> > To (un)subscribe, modify options or view archives go to:
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> > Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170811/3c2251d3/attachment.html>