Confused about specified type variables using -XTypeApplications

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Confused about specified type variables using -XTypeApplications

Ryan Scott
I read in the Visible Type Applications paper [1] that you can only
apply types to "specified" type variables. However, after trying out
-XTypeApplications, I'm confused as to what exactly that means:

    $ /opt/ghc/head/bin/ghci
    GHCi, version 8.1.20160106: http://www.haskell.org/ghc/  :? for help
    λ> :set -XTypeInType -XTypeApplications
    λ> data Prox a = Prox
    λ> let prox :: Prox a; prox = Prox
    λ> :t prox @Int
    prox @Int :: Prox Int
    λ> :t Prox @Int
    Prox @Int :: Prox a

Huh? For some reason, I'm getting different types for prox @Int and
Prox @Int! I think what's happening here is that in Prox @Int, the Int
is being applied to a kind variable. That is, it's being applied to
the k variable in:

    Prox :: forall k (t :: k). Prox t

But why is this? After all, I don't think I "specified" k anywhere in
the definition of Prox, and to make things more confusing, Int gets
applied differently in prox @Int (and the definition of prox also
doesn't mention k). Is this a bug, or am I misunderstanding something
about -XTypeApplications?

Ryan S.
-----
[1] http://www.cis.upenn.edu/~eir/papers/2016/type-app/visible-type-app.pdf
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Confused about specified type variables using -XTypeApplications

Andres Loeh-5
Hi.

I just today had a very similar problem with a kind-polymorphic class
definition. Simplified example (with ScopedTypeVariables, TypeInType,
TypeApplications):

GHCi> class C a where c :: ()
GHCi> :t c
c :: forall k (a :: k). C a => ()
GHCi> :t c @Int
c @Int :: C a => ()
GHCi> :t c @_ @Int
c @_ @Int :: C Int => ()
GHCi> let d :: forall a . C a => (); d = c @_ @a
GHCi> :t d
d :: forall k (a :: k). C a => ()
GHCi> :t d @Int
d @Int :: C Int => ()

I find it particularly confusing that GHCi prints the types of c and d
in exactly the same way, yet treats explicit type application on them
differently.

Cheers,
  Andres

On Thu, Jan 7, 2016 at 6:54 PM, Ryan Scott <[hidden email]> wrote:

> I read in the Visible Type Applications paper [1] that you can only
> apply types to "specified" type variables. However, after trying out
> -XTypeApplications, I'm confused as to what exactly that means:
>
>     $ /opt/ghc/head/bin/ghci
>     GHCi, version 8.1.20160106: http://www.haskell.org/ghc/  :? for help
>     λ> :set -XTypeInType -XTypeApplications
>     λ> data Prox a = Prox
>     λ> let prox :: Prox a; prox = Prox
>     λ> :t prox @Int
>     prox @Int :: Prox Int
>     λ> :t Prox @Int
>     Prox @Int :: Prox a
>
> Huh? For some reason, I'm getting different types for prox @Int and
> Prox @Int! I think what's happening here is that in Prox @Int, the Int
> is being applied to a kind variable. That is, it's being applied to
> the k variable in:
>
>     Prox :: forall k (t :: k). Prox t
>
> But why is this? After all, I don't think I "specified" k anywhere in
> the definition of Prox, and to make things more confusing, Int gets
> applied differently in prox @Int (and the definition of prox also
> doesn't mention k). Is this a bug, or am I misunderstanding something
> about -XTypeApplications?
>
> Ryan S.
> -----
> [1] http://www.cis.upenn.edu/~eir/papers/2016/type-app/visible-type-app.pdf
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Confused about specified type variables using -XTypeApplications

Reid Barton-2
On Thu, Jan 7, 2016 at 1:39 PM, Andres Loeh <[hidden email]> wrote:
I find it particularly confusing that GHCi prints the types of c and d
in exactly the same way, yet treats explicit type application on them
differently.

Try with :set -fprint-explicit-foralls. Maybe it should be the default when TypeApplications is enabled?

Regards,
Reid Barton

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Confused about specified type variables using -XTypeApplications

Andres Loeh-5
> Try with :set -fprint-explicit-foralls. Maybe it should be the default when
> TypeApplications is enabled?

That's indeed helpful to see the difference. Still not sure if the
(original) datatype and class-versions should have an explicit rather
than an implicit kind quantification ...

Cheers,
  Andres
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Confused about specified type variables using -XTypeApplications

Simon Peyton Jones
In reply to this post by Ryan Scott
Make a ticket?  This would be worth capturing.

I'm sure Richard will want to look at it when he gets back, and a ticket is a useful workflow organiser.

Simon

| -----Original Message-----
| From: ghc-devs [mailto:[hidden email]] On Behalf Of Ryan Scott
| Sent: 07 January 2016 17:55
| To: GHC developers <[hidden email]>
| Subject: Confused about specified type variables using -XTypeApplications
|
| I read in the Visible Type Applications paper [1] that you can only
| apply types to "specified" type variables. However, after trying out
| -XTypeApplications, I'm confused as to what exactly that means:
|
|     $ /opt/ghc/head/bin/ghci
|     GHCi, version 8.1.20160106:
| https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.haskell.o
| rg%2fghc%2f&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7caa1fba8c2743424
| c1fb008d3178bb622%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=2B1fES1XwoQb8T
| MRj7oOkfdfoGo37oXhjnHFeqgOXAI%3d  :? for help
|     λ> :set -XTypeInType -XTypeApplications
|     λ> data Prox a = Prox
|     λ> let prox :: Prox a; prox = Prox
|     λ> :t prox @Int
|     prox @Int :: Prox Int
|     λ> :t Prox @Int
|     Prox @Int :: Prox a
|
| Huh? For some reason, I'm getting different types for prox @Int and
| Prox @Int! I think what's happening here is that in Prox @Int, the Int
| is being applied to a kind variable. That is, it's being applied to
| the k variable in:
|
|     Prox :: forall k (t :: k). Prox t
|
| But why is this? After all, I don't think I "specified" k anywhere in
| the definition of Prox, and to make things more confusing, Int gets
| applied differently in prox @Int (and the definition of prox also
| doesn't mention k). Is this a bug, or am I misunderstanding something
| about -XTypeApplications?
|
| Ryan S.
| -----
| [1]
| https://na01.safelinks.protection.outlook.com/?url=http:%2f%2fwww.cis.upenn.e
| du%2f~eir%2fpapers%2f2016%2ftype-app%2fvisible-type-
| app.pdf&data=01%7C01%7Csimonpj%40064d.mgd.microsoft.com%7Caa1fba8c2743424c1fb
| 008d3178bb622%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=PKUXsuMdixF76cVq0y
| yaCW8NZbIO5hOJpXwABfUkYZw%3d
| _______________________________________________
| ghc-devs mailing list
| [hidden email]
| https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
| org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
| devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7caa1fba8c2743424c1fb
| 008d3178bb622%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=hV%2f3yHwiH36Qgegu
| hepSlx7JaZP0evwpGTTdK%2f3I3Po%3d
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Confused about specified type variables using -XTypeApplications

Ryan Scott
I've opened Trac #11376 for this: https://ghc.haskell.org/trac/ghc/ticket/11376

Ryan S.

On Thu, Jan 7, 2016 at 5:32 PM, Simon Peyton Jones
<[hidden email]> wrote:

> Make a ticket?  This would be worth capturing.
>
> I'm sure Richard will want to look at it when he gets back, and a ticket is a useful workflow organiser.
>
> Simon
>
> | -----Original Message-----
> | From: ghc-devs [mailto:[hidden email]] On Behalf Of Ryan Scott
> | Sent: 07 January 2016 17:55
> | To: GHC developers <[hidden email]>
> | Subject: Confused about specified type variables using -XTypeApplications
> |
> | I read in the Visible Type Applications paper [1] that you can only
> | apply types to "specified" type variables. However, after trying out
> | -XTypeApplications, I'm confused as to what exactly that means:
> |
> |     $ /opt/ghc/head/bin/ghci
> |     GHCi, version 8.1.20160106:
> | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.haskell.o
> | rg%2fghc%2f&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7caa1fba8c2743424
> | c1fb008d3178bb622%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=2B1fES1XwoQb8T
> | MRj7oOkfdfoGo37oXhjnHFeqgOXAI%3d  :? for help
> |     λ> :set -XTypeInType -XTypeApplications
> |     λ> data Prox a = Prox
> |     λ> let prox :: Prox a; prox = Prox
> |     λ> :t prox @Int
> |     prox @Int :: Prox Int
> |     λ> :t Prox @Int
> |     Prox @Int :: Prox a
> |
> | Huh? For some reason, I'm getting different types for prox @Int and
> | Prox @Int! I think what's happening here is that in Prox @Int, the Int
> | is being applied to a kind variable. That is, it's being applied to
> | the k variable in:
> |
> |     Prox :: forall k (t :: k). Prox t
> |
> | But why is this? After all, I don't think I "specified" k anywhere in
> | the definition of Prox, and to make things more confusing, Int gets
> | applied differently in prox @Int (and the definition of prox also
> | doesn't mention k). Is this a bug, or am I misunderstanding something
> | about -XTypeApplications?
> |
> | Ryan S.
> | -----
> | [1]
> | https://na01.safelinks.protection.outlook.com/?url=http:%2f%2fwww.cis.upenn.e
> | du%2f~eir%2fpapers%2f2016%2ftype-app%2fvisible-type-
> | app.pdf&data=01%7C01%7Csimonpj%40064d.mgd.microsoft.com%7Caa1fba8c2743424c1fb
> | 008d3178bb622%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=PKUXsuMdixF76cVq0y
> | yaCW8NZbIO5hOJpXwABfUkYZw%3d
> | _______________________________________________
> | ghc-devs mailing list
> | [hidden email]
> | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
> | org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7caa1fba8c2743424c1fb
> | 008d3178bb622%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=hV%2f3yHwiH36Qgegu
> | hepSlx7JaZP0evwpGTTdK%2f3I3Po%3d
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs