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. |
Could something like this work for you? Here, a ~ b and you have access to b: (_, proxy :: Proxy b) -> asProxyTypeOf undefined proxy :: b On Thu, Aug 10, 2017 at 4:16 PM, Wolfgang Jeltsch <[hidden email]> wrote: Hi! _______________________________________________ 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. |
In reply to this post by Wolfgang Jeltsch-3
On August 10, 2017 7:16:04 PM EDT, Wolfgang Jeltsch <[hidden email]> 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. Note that the feature described in #11350 will provide a quite direct way to accomplish this by allowing type applications in pattern matches. _______________________________________________ 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. |
In reply to this post by Michael Burge
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:
_______________________________________________ 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. |
In reply to this post by Ben Gamari-2
Am Donnerstag, den 10.08.2017, 19:39 -0400 schrieb Ben Gamari:
> On August 10, 2017 7:16:04 PM EDT, Wolfgang Jeltsch wrote: > > 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? > > Note that the feature described in #11350 will provide a quite direct > way to accomplish this by allowing type applications in pattern > matches. Yes, this feature seems to provide what I need. In my particular use case, it allows for pretty clear code. Is there also a solution that does not involve using this (unimplemented) feature? 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. |
> On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch
> <[hidden email]> 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. |
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 <[hidden email]> wrote: > On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch _______________________________________________ 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. |
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:
_______________________________________________ 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. |
Free forum by Nabble | Edit this page |