New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type-level type applications #80

Merged
merged 6 commits into from Mar 1, 2018

Conversation

Projects
None yet
10 participants
@treeowl
Contributor

treeowl commented Oct 11, 2017

Allow TypeApplications syntax to be used in types as well as
terms.

Rendered

@treeowl treeowl force-pushed the treeowl:type-level-type-app branch from 95c1de2 to 36e030e Oct 11, 2017

Type-level type applications
Allow `TypeApplications` syntax to be used in types as well as
terms.

@treeowl treeowl force-pushed the treeowl:type-level-type-app branch from 36e030e to b43bf0e Oct 11, 2017

@AntC2

This comment has been minimized.

AntC2 commented Oct 11, 2017

How does this combine with type family applications? Is this valid:

'Just @(F Int Char)

And if we allow partially applied type families?

'Just @(F Int)

What type is that?

@treeowl

This comment has been minimized.

Contributor

treeowl commented Oct 11, 2017

'Just @(F Int Char) looks perfectly sensible to me. Do you envision some sort of difficulty there?

I can't say if this would be able to handle a partially applied family, if we end up having those. Sounds a bit messy. I'd be okay with a requirement that the type argument not be a partially applied type family.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 13, 2017

If we can support partially applied type families anywhere, we can support them here. A kind argument to a type is merely an argument that needn't be specified by the user; there's nothing else special about one. This syntax gives a way to provide an argument visibly (explicitly).

I'm strongly +1.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Oct 14, 2017

I'm also supportive of this proposal, but the current write-up is a bit terse on the specifics. In particular, "Allow visible type application in types as well as terms" doesn't really give me the impression that we've thought through all of the implementation details, even though I'm sure some of you folks probably have—let's write those details down! In particular, some things I'd like to see mentioned are:

  1. Parser changes. Currently, trying to use (@) anywhere at the type level, prefix or infix, appears to result in a parse error. This actually works to our advantage here, since this means visible kind application won't steal the ability to write a type family/type synonym named (@), since GHC never granted that ability in the first place.

  2. An overview of how visibilities work for type-level things. For instance, in this term:

    {-# LANGUAGE PolyKinds #-}
    f :: forall (a :: k) b. Proxy a -> Proxy b

    There are three sorts of visibilities at play:

    1. a and b are explicitly quantified, so they're visible, and thus available for visible type application.
    2. k is implicitly quantified but still user-written, so it's specified, and also available for visible type application.
    3. The kind of b is inferred, and thus not available for visible type application.

    Will these three visibilities (and the rules for when they kick in) also apply at the type level? I suspect so, so it'd be nice to explain this with an example of something that lives at the type level, such as:

    {-# LANGUAGE PolyKinds #-}
    class C (a :: k) b
  3. Speaking of which, does a promoted data constructor inherit the visibilities of the original, term-level data constructor? That seems like a sensible choice to me, so let's explicitly state that.

  4. @AntC2 brings up an interesting point about type families. Currently, we don't allow partial application of type families, so something like this:

    type family Foo (a :: k)
    
    type Bar = Foo

    Is rejected. I assume that Foo @Type would also be rejected for similar reasons?

  5. One interesting development that's sprung out of the work on visible type applications is the need for two different variants of GHCi's :type command. There's :type, which reports the inferred type of an expression (possible after instantiating some type variables), and :type +v, which attempts to leave type variables alone as much as possible. This distinction matters for visible type application, as shown in the example GHCi session below:

    λ> :set -fprint-explicit-foralls 
    λ> :type Just
    Just :: forall {a}. a -> Maybe a
    λ> :type +v Just
    Just :: forall a. a -> Maybe a
    

    Here, only :type +v accurately reports the fact that a is available for visible type application.

    Given that this proposal wants to move TypeApplications to the kind level, what should become of the :kind GHCi command? Currently, :kind appears to behave analogously to :type +v:

    λ> :set -fprint-explicit-foralls -XDataKinds 
    λ> :kind 'Just
    'Just :: forall a. a -> Maybe a
    

    Should it remain this way? Or should we have both :kind and :kind +v to mirror :type and :type +v?

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Oct 15, 2017

  1. How should visible kind application interact with implicit quantification in type signatures? For example, in the type signature below:

    f :: Proxy (Just :: a -> Maybe a)

    The type variable a gets implicitly quantified. Should the same happen in this equivalent type signature using visible kind application?

    f :: Proxy (Just @a)

    Or should users be forced to explicitly quantify any type variable used in visible kind application?

    f :: forall a. Proxy (Just @a)
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 15, 2017

I agree with Ryan that more details are good. Though I can't speak for @treeowl, I will try to answer your questions:

  1. It seems you've concluded parsing will be easy. I agree. I do think we should allow for future-compatibility with type-level as-patterns, and so type-level @ will retain the space-sensitivity of the term-level @ (where a type application's @ must be preceded by whitespace or a comment).

  2. Your example there is slightly wrong (evidencing the need for more explanation of this). Here is the example: f :: forall (a :: k) b. Proxy a -> Proxy b. Here, a, b, and k are all specified. The fact that the quantification for a and b is explicit changes only the order that GHC uses, not whether or not the variables are available for visible type application. There are no visible tyvars there. (Contrast with data T k (a :: k), where k is visible -- that means it must be supplied at applications.)

    The rules at the kind level should be the same: variables mentioned by the user are specified; other variables are inferred.

  3. Yes, a promoted data constructor should have the same visibilities as the original.

  4. I still don't see how this feature interacts meaningfully with type families. They are orthogonal to me. Partially applied type families are, for now, utterly illegal. Nothing in this proposal changes that.

  5. I think that we got the design for :type wrong. (The default behavior should be what's currently done for :type +v, in my opinion.) I've made my case for this and lost. However, I think that :kind's behavior should mirror :type's, including the introduction of :kind +v.

  6. Mentioning a fresh type variable in a visible kind application should lead to quantification, just like any mention of a type variable does now. I personally wouldn't expect this to be detailed in the proposal.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Oct 15, 2017

2. D'oh, sorry. I meant to write required in place of visible. My bad.
4. So to be clear, Foo @Type counts as a partial type family application?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 17, 2017

Yes, if we have type family Foo (a :: k), then Foo @Type is a partial type family application and is against the rules -- just like if we had type family Foo2 k (a :: k) and were examining Foo Type.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Nov 10, 2017

@treeowl, what is the status? Are you going to integrate the comments from @RyanGlScott and @goldfirere into the proposal – or maybe one of you two wants to integrate them? Proposals are not “owned” by anyone in a strong sense, and everyone should feel entitled to improve them. You can create pull requests against branch type-level-type-app on treeowl/ghc-proposals, for example.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Nov 10, 2017

Also, the proposal should discuss whether this can happen under TypeApplications or whether it needs its own extension. (I’d hope for the former.)

@treeowl

This comment has been minimized.

Contributor

treeowl commented Nov 10, 2017

@goldfirere goldfirere referenced this pull request Dec 19, 2017

Merged

Flesh out details #1

@treeowl

This comment has been minimized.

Contributor

treeowl commented Dec 19, 2017

@goldfirere, thanks for fleshing things out. Can you comment on the potential interaction with ScopedTypeVariables I mentioned in my last comment?

goldfirere added some commits Dec 20, 2017

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Dec 20, 2017

Done -- I've just committed directly.

@treeowl

This comment has been minimized.

Contributor

treeowl commented Dec 20, 2017

@goldfirere, with ScopedTypeVariables, what happens if the kind variable is already in scope?

foo :: forall k ....
foo (x :: Foo @k) = ....

Do we verify that they match, or do we introduce a fresh k?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Dec 20, 2017

That will verify that they match -- just like occurrences of in-scope type variables in pattern signatures today. There's not really an interaction between the features here.

@goldfirere goldfirere referenced this pull request Jan 8, 2018

Merged

Explicit specificity #99

@nomeata

This comment has been minimized.

Contributor

nomeata commented Feb 23, 2018

@treeowl, @goldfirere, what’s the status of this?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Feb 23, 2018

@treeowl ? I'm ready for review here, but you're the proposer.

@treeowl

This comment has been minimized.

Contributor

treeowl commented Feb 23, 2018

@nomeata, please submit.

@nomeata nomeata merged commit 7f97482 into ghc-proposals:master Mar 1, 2018

nomeata added a commit that referenced this pull request Mar 1, 2018

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Mar 2, 2018

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Mar 2, 2018

I second the call for a list of unimplemented proposals.

Also, https://ghc.haskell.org/trac/ghc/ticket/12045 is the closest ticket that pertains to this particular proposal.

@mynguyenbmc

This comment has been minimized.

mynguyenbmc commented Jul 19, 2018

Hi, I've been working with Richard on this and now that we're close to finishing, I have a design question regarding PartialTypeSignatures warning. Currently compiling this

data T1 :: forall k1 k2. k1 -> k2 -> K.Type where
   MkT1 :: T1 j1 j2

x :: T1 @_ @(Maybe K.Type) _ _
x = MkT1

results in

compiler/Test.hs:24:9: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘w’
      Where: ‘w’ is a rigid type variable bound by
               the inferred type of x :: T1 w1 w2
               at compiler/Test.hs:25:1-8
    • In the type signature: x :: T1 @_ @(Maybe K.Type) _ _
   |
24 | x :: T1 @_ @(Maybe K.Type) _ _
   |         ^^

compiler/Test.hs:24:28: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘w1 :: w’
      Where: ‘w1’, ‘w’ are rigid type variables bound by
               the inferred type of x :: T1 w1 w2
               at compiler/Test.hs:25:1-8
    • In the type signature: x :: T1 @_ @(Maybe K.Type) _ _
   |
24 | x :: T1 @_ @(Maybe K.Type) _ _
   |                            ^

compiler/Test.hs:24:30: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘w2 :: Maybe Type’
      Where: ‘w2’ is a rigid type variable bound by
               the inferred type of x :: T1 w1 w2
               at compiler/Test.hs:25:1-8
    • In the type signature: x :: T1 @_ @(Maybe K.Type) _ _
   |
24 | x :: T1 @_ @(Maybe K.Type) _ _
   |                              ^

Should we keep it this way, or not issue warning for wildcards just like in the current term-level visible type app? Thanks.

@int-index

This comment has been minimized.

Contributor

int-index commented Jul 19, 2018

Given that the feature should be available even without -XPartialTypeSignatures (and should not allow partial type signatures in a context other than inside a @-argument), I think the -Wpartial-type-signatures flag should not control its behavior.

I see two reasonable options:

  1. disable these warnings when typechecking a @-argument
  2. add another flag, -Wpartial-type-applications, that would report these wildcards both in terms and in types

and since (1) seems easier to implement, I would postpone (2) until someone explicitly requests this feature.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Jul 19, 2018

I'm with int_index here: surely it should behave the same as term-level visible type application, whatever that is.

@mynguyenbmc

This comment has been minimized.

mynguyenbmc commented Jul 21, 2018

Thank everyone for your inputs! I have decided to go with option 1 @int-index suggested above.

@Icelandjack

This comment has been minimized.

Contributor

Icelandjack commented Sep 11, 2018

A great test of the extension would be to write every kind application explicitly in https://github.com/ekmett/eq/blob/master/src/Data/Eq/Type/Hetero.hs

@bravit bravit added the Proposal label Nov 11, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment