How to bring existentially quantified type variables into scope

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

How to bring existentially quantified type variables into scope

Wolfgang Jeltsch-3
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How to bring existentially quantified type variables into scope

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 <[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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How to bring existentially quantified type variables into scope

Ben Gamari-2
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How to bring existentially quantified type variables into scope

Wolfgang Jeltsch-3
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:
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 <[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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How to bring existentially quantified type variables into scope

Wolfgang Jeltsch-3
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How to bring existentially quantified type variables into scope

Alexis King
> 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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How to bring existentially quantified type variables into scope

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 <[hidden email]> wrote:
> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How to bring existentially quantified type variables into scope

Wolfgang Jeltsch-3
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 <[hidden email]> wrote:
> 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.

_______________________________________________
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.
Loading...