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

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 wrote:

...

...

On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch 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.