Explicit specificity

[goldfirere]

The proposal has been accepted; the following discussion is mostly of historic interest.

---

This proposal introduces new syntax typeRep :: forall {k} (a :: k). ... (the braces are new) to allow a user to quantify a variable without affecting downstream users who might use visible type application.

Rendered

[AntC2]

the braces here serve to make the argument "more invisible".

ROTFL

{ } as the cloak of more invisibility.

[treeowl]

I think this is a grand idea. I'm still a bit uncomfortable with allowing variables to be specified when they're not explicitly quantified, as in

p :: a -> b -> F a b  -- p @A @B is valid
q :: forall (a :: k). a -> G a  -- p @K @A is valid

I would generally prefer to see this effect from

p :: forall a b. F a b
q :: forall k (a :: k). a -> G a

but I recognize that being liberal about what's specified is helpful when using functions that weren't specifically written for TypeApplications but that work just fine with it anyway, and that I will probably have my head bitten off if I propose that a variable must be quantified explicitly in order to be specified.

[Ericson2314]

I think this isn't completely future-compatible? This might be valid someday:

{-# LANGUAGE NamedFieldPuns #-}
data Foo = Foo { i :: Natural }

forall (Foo { i } :: Foo) . Vec a i -> Vec a i

[treeowl]

@Ericson2314 That strikes me as somewhat surprising hypothetical syntax. Why use that instead of

forall a (foo :: Foo). foo ~ 'Foo { i } => Vec a i -> Vec a i

I mean, I guess you could argue that your way reads better, but it seems like unnecessary complication.

[simonpj]

I like this proposal. Internally, GHC already has "inferred" and "specified", but it's just inaccessible to the user. (Mind you, I always trip over nomenclature.)

The "Proposed specification" is not nearly precise enough. Beyond syntax I think we need to say

• The new inferred variables participate in the -XScopedTypeVariables feature; for example, given

f :: forall {k} (a::k). blah
f = e

both k and a scope over the right hand side e.

• In a use of Visible Type Application (-XTypeApplications), the visible type arguments instantiate only the "specified" arguments, not the "inferred" ones.

We should also specify what happens in data/class declarations.

Under "Motivation", consider this:

f :: forall a. Int -> Proxy (a::k) -> blah
f = e

In today's GHC, with -XScopedTypeVariables, the type variable a scopes over e. But so does k!!! Even though it only has occurrences (no binders) and is buried deep inside the type. This is ghastly, but is caused by the fact that initially we had no way to bind k. With TypeInType we now do; but only like this

f :: forall k a. Int -> Proxy (a::k) -> blah
-- or, stylistically better
f :: forall k (a::k). Int -> Proxy a -> blah

and now in a visible type application I'd have to specify the kind argument, which I might not want to. This proposal makes it possible to bind k without also making it a positional argument for VTA. Obviously more sensible.

[vagarenko]

Will there still be a way to specify kind parameter if needed?

If I want to apply foo :: forall {k} (a :: k). ... to say Nothing :: Maybe Bar. How do I write it?
foo @(Nothing :: Maybe Bar)?

[Ericson2314]

@treeowl

I chose my example for a reason :). It's unclear whether i is bound implicitly, or normally with a named field pun.

[int-index]

I am in favor of this proposal. (I have since reconsidered my poisition)

However, the overall design raises a question. We appear to have three levels of visibility for a parameter: visible, invisible, and super-invisible (inferred).

Is there no way whatsoever to specify the super-invisible parameters? Is this asking for a @@ syntax?

Perhaps we would want visibility levels?

0. visible
1. invisible, introduced with forall a, overriden with @
2. invisible, introduced with forall {a}, overriden with @@
3. invisible, introduced with forall {{a}}, overriden with @@@

etc

[goldfirere]

@treeowl: There was some debate about whether or not to make user-written, implicitly quantified variables available for type application. We decided "yes" in the end, but this was not an obvious choice, at the time or in retrospect. I still favor this approach as it vastly enlarges the applicability of visible type application, but I won't defend the choice staunchly.

@Ericson2314: That's an interesting new syntax. Let me expand your idea a bit. In some hypothetical language that came before Haskell (cough, cough, ML), we can imagine that pattern matching must be done explicitly:

f :: Maybe a -> Bool
f x = case x of
  Nothing -> False
  Just _ -> True

But in Haskell, we can pattern-match directly on function arguments:

f :: Maybe a -> Bool
f Nothing = False
f (Just _) = True

How convenient. You seem to be proposing (in some far-off future) that we do something similar in type variable binders. Just as the difference between my snippets above is that the latter allows pattern-matching in a variable binding position, you want to do the same, but in types. It's a reasonable idea. And if we allow type patterns to appear in type variable binding positions, I agree that the proposed syntax is indeed not future-compatible. I'm not sure how worried to be about this, but I'm glad you brought it up. Do you have any other syntax ideas?

Regardless, I've added this concern to the proposal.

@simonpj: I've added a note to the specification in the proposal that braced variables work with -XScopedTypeVariables. Your second bullet about inferred vs specified is no change from current behavior, but I now remind readers of this fact in my revised proposal. For your extra motivational example, you're assuming a change to the way scoping works, which will appear in another proposal. I don't think it's necessary to bring this change into scope here.

@vagarenko: No. If a variable is inferred, then it's not available with visible type application. Full stop. This fact keeps type inference predictable. The idea is that inferred type variables are invented by GHC, and it's conceivable that different minor versions of GHC might do it slightly differently. If there were a way to observe the ordering of inferred variables, then programs could break. Of course, these new braced variables aren't really inferred in the same way (instantiating them would be predictable), but allowing an override here but not for GHC-inferred variables leads to a system where we have specified, user-written-inferred, and truly-inferred variables in the mix, and we'd be teetering toward madness.

@int-index: You've anticipated parts of my answer to @vagarenko. No, this doesn't lead to three levels of visibility: just two. They are specified and inferred. That's it! No @@!

[goldfirere]

OK -- well, there are three levels of visibility. But visible isn't addressed in this proposal. It's addressed in #81 and doesn't interact with this proposal. In particular, forall {k} (a :: k) -> (using the syntax of #81) will be an error.

[int-index]

and it's conceivable that different minor versions of GHC might do it slightly differently.

Okay, so let us consider the visibility levels model I mentioned earlier:

0. visible
1. invisible, introduced with forall a, overriden with @
2. invisible, introduced with forall {a}, overriden with @@
3. invisible, introduced with forall {{a}}, overriden with @@@

In this model, we could also talk about infinity-level (inferred) — those variables can be introduced by GHC exclusively, and there is no possibility for an override.

After this proposal we have an asymmetry: the users can introduce the inferred variables, but cannot override them. This is not a deal breaker, but the abstraction is leaking.

[goldfirere]

What abstraction is leaking? I see an asymmetry, but I don't see a leaky abstraction.

[int-index]

The abstraction (to my understanding) is that the "inferred" level is an implementation detail for GHC. Now it's leaking to the user-facing language (the ability to write forall {a}) — yes, out of necessity, but so is the case with other abstraction leaks. And the asymmetry is more evidence that it's a leak.

(Once again, I'm in favor of the proposal, I see the need for it, just sharing an observation that bothers me a bit)

[goldfirere]

OK -- I can see what you're getting at now, and I see why it's bothersome. But I don't think we can do better.

[int-index]

But I don't think we can do better.

Can we ensure that the variables introduced by the user with the forall {k} syntax are the same as what GHC might have inferred? So this would be a means to access inferred variables, not to introduce them.

[int-index]

Since GHC infers these type variables, this is similar to partial type signatures, which GHC infers also.

In the motivation section, we have this example:

typeRep1 :: Typeable a => TypeRep a
typeRep2 :: Typeable (a :: k) => TypeRep (a :: k)

With -XPartialTypeSignatures we can rewrite it as:

typeRep3 :: Typeable a => TypeRep (a :: _)

And then introduce named partial type signatures, which allow access to whatever GHC infers:

typeRep3 :: Typeable a => TypeRep (a :: (k = _))
                                         ^
                                    this is a binding
                                    site for 'k'

(the syntax is hypothetical)

Now k is whatever GHC infers, and can be used in -XScopedTypeVariables. This is also more general because the inferred type need not be a variable. And it's entirely orthogonal to -XTypeApplications, where the abstraction barrier is preserved.

[vagarenko]

@goldfirere

No. If a variable is inferred, then it's not available with visible type application.

But I didn't use visible type application for the inferred variable in my example:

If I want to apply foo :: forall {k} (a :: k). ... to say Nothing :: Maybe Bar. How do I write it?
foo @(Nothing :: Maybe Bar)?

I use type application for a variable, not k and give it kind Maybe Bar via type annotation. I'm asking will this continue to work? It works in GHC-8.2.1:

>:set -fprint-explicit-kinds
>:t Proxy @'Nothing
Proxy @'Nothing :: forall {a}. Proxy (Maybe a) ('Nothing a)
>:t Proxy @('Nothing :: Maybe Int)
Proxy @('Nothing :: Maybe Int) :: Proxy (Maybe Int) ('Nothing Int)

[goldfirere]

@int-index: You are suggesting replacing

typeRep :: forall {k} (a :: k). Typeable a => TypeRep a

with

typeRep :: forall (a :: (k = _)). Typeable a => TypeRep a

where the k would scope over the implementation of typeRep. However, these two type signatures mean different things: the first requires that the kind of a be abstract, while the second allows a's kind to be inferred to be something other than a variable. Furthermore, your proposed k = _ syntax isn't necessary: see NamedWildCards.

Bottom line: I don't think this is an adequate replacement for this proposal.

@vagarenko: Ah, I understand better now. Yes, that would still work. This proposal is all about how to write types to work the desired way with visible type application.

[int-index]

However, these two type signatures mean different things: the first requires that the kind of a be abstract, while the second allows a's kind to be inferred to be something other than a variable.

Well, that's the point (sort of). Rather than add another mechanism to introduce variables, we just use "whatever GHC infers", which might not be a variable (I don't see how it's problematic).

Furthermore, your proposed k = _ syntax isn't necessary: see NamedWildCards.

That's good news, thanks!

Bottom line: I don't think this is an adequate replacement for this proposal.

Okay, but can you add it to alternatives? There's probably a use case where this alternative wouldn't work, but I can't come up with one.

[Bj0rnen]

What's the argument for adding this syntax instead of allowing to declare type variables out of dependency order natively? With that, no special syntax would be needed, and you could effectively "hide" type variables just by putting them last.

It seems to me like support for that would only require a trivial amount of sugar on top of what this proposal does. At least this example made it seem that way:

typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a

So what if you could just write that as below?

typeRep4 :: forall (a :: k) k. Typeable a => TypeRep a

Internally it could be implemented using the proposed hiding mechanism without having to expose that as a language feature. Some care has to be taken to not expose the k' variable or the k ~ k' constraint that would be generated in any error messages, etc. Not that there would need to be a full-blown implementation of the proposed feature anyway.

1. Is it actually always trivial to desugar out-of-dependency-order type variables into the synatx proposed here?
2. Does pure hiding add something to the table which free reordering doesn't?

[Ericson2314]

@goldfirere

Do you have any other syntax ideas?

@Bj0rnen

That's nice, but anti-modular. Say you are using a type alias:

old :: OldFoo -- OldFoo is higher ranked, so old takes type arguments
backCompat :: forall {a}. NewFoo a

Admittedly, this came out more contrived than I thought, but the basic idea is if some quantifiers are abstracted away, it's not easy to rearrange them.

[Ericson2314]

Overall, I am sort of getting the same cat-and-mouse vibes between introduction and elimination as @int-index with the @@@... examples. The motivation is compelling, and I can't think of another solution, but the situation overall seems tragic.

[goldfirere]

I'm intrigued by @Bj0rnen's idea. It can be backward-compatible: as long as a library doesn't change existing type parameters, that library can always add new ones at the end of a list. I'm not convinced by the anti-modular argument @Ericson2314 puts forward. Implementing this idea seems very difficult, unfortunately. (Currently, GHC uses the same types in Core as it does in Haskell, and @Bj0rnen's idea means we either have to stop doing this or somehow encode a transformation between them.) I'd be curious for more feedback on this idea.

[goldfirere]

I've added @Bj0rnen's idea as an alternative, and I argue there why I think the main proposal is still the best way forward.

[int-index]

@goldfirere What's a use case that scoped NamedWildCards for a kind would not cover, but the current proposal would?

Bottom line: I don't think this is an adequate replacement for this proposal.

[AntC2]

I see @yav has posted some (useful) questions for clarification about how the proposal works on the Committee mailing list.

Could I ask that such questions and their answers appear in this discussion thread. (And possibly get incorporated into the proposal text, if it's unclear/incomplete.)

I appreciate it's often difficult to separate out aspects of the discussion but as a rule of thumb: here is about the what and how; the Committee discussion should be only about the why and why important/worthwhile, and assuming those Committee members who post have already absorbed the proposal. (At least, that's how I understand it.)

[int-index]

It still bothers me that, assuming we get forall ->, this leaves us with these variations:

• type variables that are visible by default, forall a ->
• type variables that are invisible by default but can be overriden, forall a.
• type variable that are invisible and cannot be overriden, forall {a}.

This means that we have a language mechanism to override visibility at call site, and then another mechanism to say "no, this variable visibility cannot be overriden". I fail to see why we stop at this point and do not introduce the next level, "yes, I do want this variable visibility to be overriden", ad infinitum.

This leads us to the design I outlined in #99 (comment)

As long as we don't introduce forall {a}., we have the wiggle room to retreat and consider things like named type applications, for which I argue in #99 (comment)

I would like to avoid committing to the current suboptimal solution by exposing its syntax to the user.

[simonpj]

It still bothers me that, assuming we get forall ->, this leaves us with these variations:

1. type variables that are visible by default, forall a ->
   

2. type variables that are invisible by default but can be overriden, forall a.
3. type variable that are invisible and cannot be overriden, forall {a}.

It seems to me that we are more or less forced into this design:

1. Some arguments are compulsory. When we write Maybe Int we must write the Int. We can't write Maybe and expect the Int to be inferred.
2. We want visible type application. It's in GHC now and it's extremely useful.
3. But currently we can write type signatures that do have explicit foralls but that do not quantify, or even mention, all their kind variables. We can't reasonably use visible type application for these because their order is so unconstrained.

I suppose that we could declare class (3) empty, by rejecting any typethat has variables that are not explicitly mentioned, and thus live in class (3). So then

data Proxy a = Proxy

would not be poly-kinded -- instead I suppose it'd default to kind Type. To get the poly-kinded version you'd have to write

data Proxy (a :: k) = Proxy

And I suppose that might not be a bad thing.

But what about term-level functions whose type is inferred? (A bit like Proxy, but at the term level.) We clearly still have to accept functions without a type signature. But (in the current design) their type variables are in category (3) and we can't use visible type application.

[AntC2]

But what about term-level functions whose type is inferred? (A bit like Proxy, but at the term level.) We clearly still have to accept functions without a type signature. But (in the current design) their type variables are in category (3) and we can't use visible type application.

I think we have a general (but probably informal) rule that if you want to use 'fancy' type features, you must put a type signature. This is in line with Hindley-Milner inference, which never requires a signature.

2. We want visible type application. It's in GHC now and it's extremely useful.

Yes and yes. Speaking as somebody still trying to get my head round type application, I always feel nervous about the canonical sequence of arguments. Having to guess it for tokens that don't even have a signature strikes me as too hard. As it is, you have to pay attention it's not as simple as left-to-right appearance of variables in a signature.

Then you're implying a rule that seems sensible: to use type application, put a signature; if that's poly-kinded type application, that signature must mention variables for the kinds.

[simonpj]

Then you're implying a rule that seems sensible: to use type application, put a signature; if that's poly-kinded type application, that signature must mention variables for the kinds.

Yes, that's the rule today. int-index is sad to have three categories, and I sympathise. But I'm just pointing out that it's hard to make do with two. If anyone has an idea for how to make do with two, that would be great: let's see it.

[AntC2]

it's hard to make do with two [categories].

(Must admit I've lost the plot on all the options swirling around here; and I've just read the 'Type Variables in Patterns' paper ...)

Can't we resort to type signatures in patterns, and thereby 'reach' any type/kind, even if we can't reach it via type applications? To take your Proxy without explicit kind

data Proxy a = Proxy                          -- I'm importing this, so can't change it

f :: Proxy (a :: k) -> blah ... a ... k ...
f (x :: (Proxy (aa :: kk))) = ... aa ... kk ...

(I've used distinct tyvars there for the pattern, to show there's nothing up my sleeves. Or is TVIP proposing to deprecate the PatternTypeSignatures bit of ScopedTypeVariables? I do see it's going to be confusing having so many similar-but-different ways to express typing.)

The TVIP paper points out pattern signatures can be clumsy/ugly. (Presumably this arises because the code wanting to put signatures is importing something not declared with type applications in mind.) There is a case [paper section 3.6] where it's impossible to specify a suitable pattern signature. But the paper's proposing a way to express that with type applications. It's an existential GADT with a type family; so falls well within my 'fancy' features; then there has to be a signature. (And hooray for doing away with Proxy.)

[goldfirere]

I've updated this proposal to remove the ability to put braces in the tyvars in a class head, in favor of new proposal #148.

[nomeata]

I am still undecided whether I like this approach (encoding specificity in the type) or would rather see that as separate declarations (like we do for the roles of type constructor). But I think I know what questions I have to ask to make up my mind:

Will the following work:

-- specificity in a higher rank position
foo1 :: (forall {a} b. a -> b -> a) -> Int
foo1 g = g @String 0 "Hi"

-- specificity overriden by type annotation
foo2 :: Int
foo2 = (const :: forall {a} b. a -> b -> a) ) @String 0 "Hi"

-- partial application
foo3 :: Int
foo3 = h @String (True, "Hi")
  where
    h = g 0
    g :: forall a. a -> (forall {b} c. (b,c) -> a)
    g x _ = x

If the answer is “yes”, then I agree with putting the specificity into the types, because it behaves like types.

If the answer is “no”, ans specificity is really a property of “the $n$-th type argument of a concrete, bound function”, then I am inclined to advocate for a separate declaration (like roles). This would also avoid stealing the {…} syntax in types, which may be valuable in the future, and obviate the need for different printing modes in :t because specificity could be reported in :info name.

I could not answer these questions clearly from the spec, which may mean that the spec could be refined to do so. (Or I missed the crucial bit if its there, which is possible :-))

NB: Coq has both forms of declarations ({a} in types, Arguments command), but does not support it in higher rank contexts, which I found a unsatisfying experience.

[goldfirere]

In response to #99 (comment)

• foo1 is accepted.
• foo2 is accepted.
• foo3 is rejected. In no change from the status quo, all let-bound definitions are instantiated and regeneralized en route to determining their types. Thus, h gets the type forall {a} {b} {c}. Num a => (b, c) -> a and is not available for visible type application.

In other words, these really are types, not some other construct.

[nomeata]

Thanks!

[chshersh]

I appreciate this proposal as well. Just today I really needed the feature. I will describe my use-case below.

Problem description

I have data type parameterized by type variable polymorphic in kind:

data TypeRepMap (f :: k -> Type) ...

And I would like to write the following code:

lookup :: forall a f . TypeRepMap f -> Maybe (f a)
lookup = ... some implementation here ...

member :: forall a f . TypeRepMap f -> Bool
member trMap = case lookup @a trMap of
    Nothing -> False
    Just _ -> True

Unfortunately, this code doesn't compile with the following error:

    • Couldn't match type ‘f’ with ‘f0’
      ‘f’ is a rigid type variable bound by
        the type signature for:
          member :: forall k1 k2 (a :: k2) (f :: k1 -> *).
                    Typeable a =>
                    TypeRepMap f -> Bool
        at internal/Data/TypeRep/CacheMap.hs:116:1-57
      Expected type: TypeRepMap f0
        Actual type: TypeRepMap f
    • In the second argument of ‘lookup’, namely ‘trMap’
      In the expression: lookup @a trMap
      In the expression:
        case lookup @a trMap of
          Nothing -> False
          Just _ -> True

Workaround 1

Change type of member function with explicit kind annotation:

member :: forall k (a :: k) (f :: k -> Type) . TypeRepMap f -> Bool

I don't like this workaround because every time I call member function I need to do it like this:

member @_ @Int

instead of just member @Int.

Workaround 2 (current solution)

This solution was proposed by @int-index. It makes interface better but messes up with documentation

type KindOf (a :: k) = k

member :: forall a (f :: KindOf a -> Type) . TypeRepMap f -> Bool

Maybe somebody knows better solution?

If current proposal is implemented then I can just write the following (without introducing custom types):

member :: forall {k} (a :: k) (f :: k -> Type) . TypeRepMap f -> Bool