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

[Wolfgang Jeltsch]

Hi!
I think this is too complicated. I am developing a library and this
access to existentially quantified type variables is something that
cannot be part of the library, but must be done by users using the
library. So it should be doable in an easy-to-understand and lightweight
way.
All the best,
Wolfgang
Am Freitag, den 11.08.2017, 07:04 +0000 schrieb Kai Zhang:
> How about this:
> 
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE GADTs #-}
> 
> import Data.Proxy
> 
> data IsListType a where
>     IsListType :: IsListType [b]
> 
> type family Elem a where
>     Elem [a] = a
> 
> elemType :: forall a b . Elem a ~ b => IsListType a -> Proxy b
> elemType _ = Proxy :: Proxy (Elem a)
> 
> On Thu, Aug 10, 2017 at 5:29 PM Alexis King <lexi.lambda at gmail.com>
> wrote:
> > > On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch
> > > <wolfgang-it at jeltsch.info> wrote:
> > >
> > > Is there also a solution that does not involve using this
> > > (unimplemented) feature?
> > 
> > I get the feeling there is a better way to do this, but I found
> > something of a hack that I think does what you want. Using
> > Data.Type.Equality, you can match on Refl to bring the `b` into
> > scope.
> > 
> >   import Data.Type.Equality
> > 
> >   f :: forall a. IsListType a -> ()
> >   f IsListType = case Refl of
> >     (Refl :: (a :~: [b])) -> ()
> > 
> > This is sort of silly, though.
> > 
> > Alexis
> > 
> > _______________________________________________
> > 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/6237ad76/attachment.html>