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: 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
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 <ryan.gl.scott@gmail.com> 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 ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
On Thu, Jan 7, 2016 at 1:39 PM, Andres Loeh <mail@andres-loeh.de> 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
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
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:ghc-devs-bounces@haskell.org] On Behalf Of Ryan Scott | Sent: 07 January 2016 17:55 | To: GHC developers <ghc-devs@haskell.org> | 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.... | 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.... | 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 | ghc-devs@haskell.org | 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
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 <simonpj@microsoft.com> 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:ghc-devs-bounces@haskell.org] On Behalf Of Ryan Scott | Sent: 07 January 2016 17:55 | To: GHC developers <ghc-devs@haskell.org> | 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.... | 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.... | 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 | ghc-devs@haskell.org | 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
participants (4)
-
Andres Loeh -
Reid Barton -
Ryan Scott -
Simon Peyton Jones