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

Top-level kind signatures (instead of CUSKs) #54

Merged
merged 6 commits into from Sep 30, 2018

Conversation

Projects
None yet
@goldfirere
Contributor

goldfirere commented Jun 6, 2017

Rendered

@nomeata

This comment has been minimized.

Contributor

nomeata commented Jun 6, 2017

The proposal might want want to justify type over kind. A Haskell programmer that is less deep into dependently typed stuff might know about kinds, but not quite think of them as “just types”, and he’d surely expect

kind Monad : (* -> *) -> Constraint
class Monad m where …

instead of

type Monad : (* ~> *) ~> Constraint
class Monad m where …

This question might also indicate that the variant without a keyword might be better.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jun 6, 2017

I'm not quite sure this proposal sits well with me. It goes through a lot of engineering to dodge the fact that GHC's kind inference doesn't behave how one might expect in certain corner cases. Granted, these corner cases might become more prevalent as dependently typed programming in Haskell becomes more popular, but for now I'd say they're a minority of programs.

Here's an alternative that I didn't see discussed in the proposal: why not have a pragma {-# CUSKs #-} that mandates the use of complete-specified kind signatures? That is, this:

{-# LANGUAGE CUSKs #-}
-- Whatever other extensions you need...

data T :: forall k. k -> Type

would become an error. (Optionally, the error message could help you by telling you to put a kind signature on k.) And if you try to do something fancy like polymorphic recursion at the type level, GHC could suggest the use of CUSKs to help you out.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jun 7, 2017

@nomeata: But you're giving a signature to a type, not a kind. That is, the thing appearing right after the word type is indeed a type. So I still favor type here. (Never mind that type is already a keyword.)

@RyanGlScott: Agreed that this is for a tiny minority of programs. Discussing the size of the sample set seems to suggest that we just live with the status quo.

As for your alternative, should I understand that to mean: GHC will check for CUSK syntax on every declaration. If it doesn't have CUSK syntax, then reject.

That seems like to broad a brush. A variation on that theme might be to have a per-declaration {-# CUSK T #-} pragma that tells GHC that T has a CUSK. Then, if GHC can't figure out the kind of T sufficiently before looking at T's definition, reject. That would be considerably simpler than my proposal. I still prefer the tenor of my proposal because it lines types up with terms. But perhaps this alternate will do. I will update the proposal.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jun 7, 2017

I've updated the proposal. If there is popular support for this new variant, I could flesh it out into a proper specification.

@nomeata

This comment has been minimized.

Contributor

nomeata commented Jun 7, 2017

@nomeata: But you're giving a signature to a type, not a kind. That is, the thing appearing right after the word type is indeed a type. So I still favor type here. (Never mind that type is already a keyword.)

Ah, I see the reasoning. It is “(type foo) has signature bar”, not “on the kind level (the signature of foo is bar)”. But that only proves my point that this can confusion.

Now that I think about it, I always read

type Age = Int

as

This is a type synonym defined by the equation Age = Int

i.e. with = binding more tightly than type. But your comment prompted me to read that as

The type Age is defined to be Int.

In that light, explicit type annotations should have been foo (type Int), but that is of course too chatty. But we can take the reverse, and allow

@Monad :: (* → *) → Constraint

and then go all the way and allow

@Age = Int

for type synonyms. And by now I have long gone astray… :-)

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Jun 7, 2017

A variation on that theme might be to have a per-declaration {-# CUSK T #-} pragma that tells GHC that T has a CUSK. Then, if GHC can't figure out the kind of T sufficiently before looking at T's definition, reject. That would be considerably simpler than my proposal.

If there is popular support for this new variant, I could flesh it out into a proper specification.

Obviously, +1 from me. I'd add that I'd like a way to automatically apply a {-# CUSK #-} pragma to every top-level declaration in a module that supports one, for the sake of convenience.

I still prefer the tenor of my proposal because it lines types up with terms.

I can see why you'd prefer that, but I feel that this proposal overshoots the goal of "lining types up with terms", since in many cases, adding top-level kind signatures introduces a fair bit of redundancy. For instance, this happens with GADTs:

type MonoTagged :: Type ~> Type ~> Type
data MonoTagged a b where
  MonoTagged :: x -> MonoTagged t x

Since the top-level kind signature now completely specifies the kinds of MonoTagged's type variables, the variables a and b are now completely redundant, since they don't reveal any kind information, and they don't scope over any constructors. A similar issue occurs for the top-level type variables for type families.

This is why I much prefer the {-# CUSK #-} proposal, since you'd have instead:

{-# CUSK MonoTagged #-}
data MonoTagged :: Type -> Type -> Type where
  MonoTagged :: x -> MonoTagged t x

Which is far less redundant, and it also has the added bonus of not needing to worry about whether you need to use (->) or (~>), which is something that I'd prefer not to think about unless I'm working with type families.

@Icelandjack

This comment has been minimized.

Contributor

Icelandjack commented Jun 7, 2017

Similar to GHC Trac #11620

@Ericson2314

This comment has been minimized.

Ericson2314 commented Jun 7, 2017

Could we instead require/treat declarations in the form

data MonoTagged :: Type -> Type -> Type where
class Bar :: Type -> Type -> Constraint where

(i.e. without parameters) as CUSKs, skipping the need for {-# CUSK ... #-} or an extra redundant line?

I'd like that, or

type MonoTagged :: Type ~> Type ~> Type
data MonoTagged where
  MonoTagged :: x -> MonoTagged t x
@Icelandjack

This comment has been minimized.

Contributor

Icelandjack commented Jun 7, 2017

@Ericson2314 Does class not need to bind variables, this doesn't look right

class Functor :: (Type -> Type) -> Constraint where
  fmap :: (a -> b) -> (f a -> f b)
@Ericson2314

This comment has been minimized.

Ericson2314 commented Jun 7, 2017

oops, good point :)

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jun 7, 2017

@nomeata: You seem to be using @ as a shorthand for "type". I always think of it as an invisibility-override, making something normally invisible to be visible. Right now, there is an overlap between these definitions. But not forever. :)

Others: Yes, there is redundancy. I could see dropping the requirement that GADTs and type families drop their scope-less variables... but annoyingly, classes would have to keep them, as they have a scope.

@Ericson2314: The problem with labeling

data Foo :: Type -> Type -> Type where ...

as having a CUSK is that it introduces a new syntactic rule, something I'm trying to get away from. It's just one more thing to specify and implement.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Jun 7, 2017

@goldfirere yeah to be clear, I like your proposal, and I want to unify things as much as possible in addition to getting rid of weird rules. Just was trying to think of something---too quickly it seems :)---in response to others' concerns.

I wonder if the scoped type variables extension can provide any inspiration. Currently we can do

f (x :: Int) = 1

but not

f (x :: Int) :: Int = 1 -- bad

and also not polymorphic recursion

f (x :: a) = True && f      1 && f      [] -- bad
f (x :: a) = True && f @Int 1 && f @[a] [] -- bad

I wonder if, just as you speculate visible type quantification can help with impredicativitiy in your thesis, we could someday check

f (@a :: type) (x :: a) = True && f @Int 1 && f @[a] [x]

or infer

f @a (x :: a) = True && f @_ 'c' && f @_ [x]

My favorite style of declaration would be, were it was available:

foo :: Bar -> Baz = \case
  ..

to avoid any replication of identifiers or first-order-specific sugar. But this notation doesn't generalize to data and class, at least without some generative lambda which is a ridiculously huge can of worms on it's own.


I guess my conclusion form all that meandering is: let's do things something like the proposal, but in addition the 1-line CUSK rules becomes a bit more palatable if they are valid for each sort of declaration.

@AntC2

This comment has been minimized.

AntC2 commented Jun 16, 2017

Sorry to ask a dumb question, but I don't see what 'problem' this is addressing. To take the opening examples, can't we write those like this? (Apart from the twiddly arrow.) I've commented out the proposed what-I-think-of-as kind signature:

-- type MonoTagged :: Type ~> Type ~> Type
data MonoTagged (t :: Type) (x :: Type) = MonoTagged x :: Type

-- type Id :: forall k. k -> k
type family Id (x :: k) :: k where
  Id x = x

-- type C :: (k ~> Type) ~> k ~> Constraint
class C (a :: k -> Type) (b :: k) where     -- :: Constraint implied by class
  f :: a b

If you're going to say: we should be able at the type :: kind level to parallel giving signatures at the term :: type level; then: no, at the term level you don't have to give stand-alone signatures, you can put them in line against the parameters and result.

So how often do Haskellers need to write (tricky) kind signatures?

Or if these what-I-think-of-as kinds are really types, we could allow:

MonoTagged :: Type -> Type -> Type    -- no keyword

Ok that starts with upper case, so is not a term signature; but we already do that in GADTs:

data Term a where
    Lit    :: Int -> Term Int
    ...

So:

data MonoTagged  (x :: Type) :: Type where
  MonoTagged ::  (t :: Type) ~> (x :: Type) ~> MonoTagged (x :: Type)
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jun 16, 2017

@Ericson2314: The problem is that we can't really use polymorphic recursion unless we know all the parts of a type. So your examples don't work (even if GHC were to be more liberal in this regard): you would need to annotate the return-type as Bool. I'm sympathetic to your desire to avoid repetition -- and my suggested syntax is indeed repetitive -- but I think your examples try to port the current wonky, fiddly type-level story down to the term level.

@AntC2: The fundamental question is: when do we allow polymorphic recursion? Henglein's 1993 paper "Type inference with polymorphic recursion" tells us that inferring polymorphic recursion is undecidable. Standard Haskell and GHC take the approach that polymorphic recursion is allowed (in terms) only when a type signature (without any wildcards) is provided. However, we still must ask: when do we allow polymorphic recursion in types? After much debate, we decided on a set of syntactic rules that tell us when to allow polymorphic recursion in types. The problem is that these rules are fiddly and confusing, resulting in a slow trickle of bug reports (some even by Simon and me!) written by users thinking that GHC is making a mistake. This proposal simplifies the state of play, making it clearer when polymorphic recursion is allowed (only when a top-level kind signature is provided).

The proposed syntax for this has redundant elements, as @Ericson2314 rightly points out. Concrete suggestions for improvement are very welcome.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jun 16, 2017

I didn't review my comment before finishing. I should also include:

The examples @AntC2 gives are accepted today. None of them use polymorphic recursion, so there is no need for the kind annotations. They would be accepted also under this proposal. The problem is only definitions with polymorphic recursion, where a kind variable has a different value in a recursive use than in the head.

@AntC2

This comment has been minimized.

AntC2 commented Jun 16, 2017

Thanks @goldfirere

The examples @AntC2 gives are accepted today. None of them use polymorphic recursion, ...

(I took them from the proposal, thinking you meant them to illustrate the point.)

OK so can we beef up the proposal text with an example of polymorphic recursion that you can't write today? And/or where providing a top-level kind signature would make a difference.

@AntC2

This comment has been minimized.

AntC2 commented Jun 16, 2017

Edit: I added more comments ~4 hours after orig. post. Also I'll add a link from #52 (Partially applied type families).

(I keep being told the objective is to make type/kind level programming more like term/type level.)

Re the twiddly arrow: is matchability something that applies between arguments? Or does it apply to an argument itself? Could I mix -> and ~> in the same signature/KindAscription? (For example a -> b ~> c ~> d to mean the first two arguments must be supplied but the third can be omitted/supplied elsewhere.) What would that mean?

Does a ~> b mean that both args are matchable, or only one (which?). If both then for a class, what does ... ~> Constraint mean? The result must be kind Constraint.

And if I can't mix, then ~> vs -> is something that applies for the whole signature, not elements of it(?) So the syntax is not a good fit to the abstraction.

(It's difficult to find a parallel at term level: any function or data constructor can be partially applied.)

In particular if the idea is to provide for injectivity (wot terms do not 'ave), beware that the current injectivity is at a half-way stage (IIUC); the end game is to take result + some args to improve other args.

I'm wondering if matchability is more like an irrefutable pattern ~(x: xs)(?) or like an equality constraint ( F a ~ b)(?) That is semantics: first match the bare argument by syntactic position, then improve from other arguments. Then what about this syntax:

type C :: ~(k -> Type) -> ~k -> Constraint
class C a b where
  f :: a b

Or if signature not neede for the class/instance level:

class D a b ~(F a b) where ...
instance D a b ~(F a b) where ...

Instead of:

class (F a b ~ c) => D a b c where ...
instance (F a b ~ c) => D a b c where ...

As suggested

@mniip

This comment has been minimized.

mniip commented Jun 16, 2017

Re the twiddly arrow: is matchability something that applies between arguments?

Yes. It's not a property of either argument, but rather the property of the function.

Could I mix -> and ~> in the same signature/KindAscription? (For example a -> b ~> c ~> d to mean the first two arguments must be supplied but the third can be omitted/supplied elsewhere.) What would that mean?

If we follow Richard's notation (matchable ~>) then the kind you describe is what today haskell would call a single argument type family returning a two-parameter datatype. You cannot distinguish type functions of such kind, but once you saturate them with one argument they become matchable type constructors.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Jun 16, 2017

@goldfirere Fair point with explicit return types, though I would like to support those those too. I'm not terribly concerned about the repetition in fact; I just want use to have as uniform a syntax as possible. Even if neither data Foo (a :: Bar) :: Baz where ... or foo (a :: Bar) :: Baz = ... is considered fully explicit, if one is valid syntax I'd like the other to be too. Likewise, I like your proposal because since we already support redundant syntax for terms:

foo :: Bar -> Baz
foo (x :: Bar) = ...

we should support it for types.

I suppose then that those other aspects of syntax consistency can wait for another RFC, as this one is really about getting rid of CUSKs. The only other thing I'd propose as part of this RFC is a limited form of what I original thought of:

type MonoTagged :: Type ~> Type ~> Type
data MonoTagged _ _ where
  MonoTagged :: x -> MonoTagged t x

to be allowed with any data definition using GADT syntax, though IMO best style in conjunction with these top level signatures.

@AntC2

This comment has been minimized.

AntC2 commented Jun 18, 2017

Re the twiddly arrow: is matchability something that applies between arguments?

Yes. It's not a property of either argument, but rather the property of the function.

So let me see if I'm getting this. Once a ~> appears, all arrows to its right [**] must be ~>(?) IOW this is wrong:

type F :: a ~> b -> c ~> d
type family F ...

And yet [Proposed Change 2.] says

Any arguments to the left of ->'s must be arguments to the type family that must be saturated at every occurrence.

So what does a count as in the above signature of F? It is "to the left of" an ->, but not immediately to the left.

Note [**]: I'd better be careful about what I mean by "to its right". I mean, at the same level in the sig. Then nesting other arrows are OK(?) Like this or this:

type C :: a ~> (b -> c) ~> d     -- -> is to right of ~>, but -> is nested
class C ...
type G :: a -> (b ~> c) -> d     -- -> is to right of ~>, but ~> is nested
type family G ...

Q to self: at the term level, data constructors are both generative and injective. Yet we don't have two styles of arrow. Why not?

  1. We're not trying to solve equality of terms algebraically at compile time.
    (That's what run-time is for.)
  2. There's a lot more complex possible comparisons between terms than equality. And those tell us nothing about generativity/injectivity.
  3. Terms have nothing to parallel unification: 'refining'/'improving' values until they're equal.
@nomeata

This comment has been minimized.

Contributor

nomeata commented Aug 3, 2017

There wasn’t any discussion here for a while. What is the status of this proposal?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Aug 3, 2017

Still under active consideration. I've been trying to get this on @simonpj's radar, but that hasn't happened -- too many other places to play. Some requests for clarification (esp. better examples) above are helpful. I will address these in due course.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Aug 25, 2017

My thoughts

  1. I think the twiddly-arrow thing is a huge distraction. I have no idea when we'll introduce partially applied type functions, if ever. If/when we do, we may want twiddly arrows, but they'll probably have to show up in lots of places. And we might do something else instead; we can't know until we get there. People already use twiddly arrows for their own purposes. I would need serious convincing that the (immediate, certain) short term pain is justified by the (deferred, uncertain) long term gain.

  2. I like the basic proposal a lot. The whole CUSK thing is a mess. And I often find myself writing out the kind signature anyway! Much better to have the written-out version mechanically checked :-).

  3. There should definitely be a type intro word, else it looks like a type signature for a data constructor.

  4. At the term level, the explicit forall's from the type signature scope over the term definition. So for consistency, the explicit forall's from the kind signature should scope over the type definition.

  5. The proposal should state that the rules for adding implicit foralls are the same as those for type signatures.

Let's do it. No twiddly arrow.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Aug 28, 2017

I agree that the twiddly arrow is distasteful (especially before the future comes).

But we can't implement @simonpj's suggestions directly: we still need to distinguish the kind signatures for these two:

type family F1 (x :: Type) :: Type -> Type
type family F2 (x :: Type) (y :: Type) :: Type

The first has one argument; the second has two. I don't think they can have the same signature. So we need some syntax. The reason I've suggested the twiddly arrow is that it seems forward-compatible. If we ignore the distinction between matchable and unmatchable arguments here, we'll have an annoying backward-compatibility problem later, I think. If someone else has a less-strange forward-compatible idea, I'm all ears.

(By the way, @AntC2 was right in that type F :: Type ~> Type -> Type would be illegal: the first argument is matchable while the second isn't. GHC doesn't support that. Yet.)

@simonpj

This comment has been minimized.

Contributor

simonpj commented Aug 29, 2017

I suppose you're arguing that this is a bloody mess, and so we shouldn't wait until it's sorted before proceeding with eliminating CUSKs. Maybe I've just convinced myself that you're right.

I could not have said it better myself. If there was a simple, clear, obviously-right future plan then we might want to future-proof ourselves against it. But alas there isn't, so let's not hold up the ship for it. (I'm optimistic: things often become clearer with time.)

@AntC2

This comment has been minimized.

AntC2 commented Aug 29, 2017

Replying to @goldfirere

I agree that the twiddly arrow is distasteful (especially before the future comes).

What's wrong about it is that you're trying to express a characteristic of the whole signature, whereas an arrow appears between two particular arguments to the function.

But we can't implement @simonpj's suggestions directly: we still need to distinguish the kind signatures for these two:

type family F1 (x :: Type) :: Type -> Type
type family F2 (x :: Type) (y :: Type) :: Type

The first has one argument; the second has two. I don't think they can have the same signature. So we need some syntax.

The syntax needs to say there's a break point between the first and second vs between second and third arguments. It's a kinda strictness annotation: the caller must strictly provide arguments up to some point (so that GHC can evaluate the TF call). A wild suggestion for syntax that looks sufficiently arresting:

F1 :: Type ! -> Type -> Type
F2 :: Type -> Type ! -> Type

The reason I've suggested the twiddly arrow ...

I think it's wrong to decorate the arrow. You need to decorate the argument position.

(By the way, @AntC2 was right in that type F :: Type ~> Type -> Type would be illegal: the first argument is matchable while the second isn't. GHC doesn't support that. Yet.)

Does your "yet" mean that signature might be legal one day? On that day can we freely mix arrows in any positions?

G :: Type ~> Type -> Type ~> Type -> Type
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Aug 29, 2017

I maintain that matchability is a property of the arrow. It just so happens that GHC doesn't support unsaturated unmatchable type-level functions -- otherwise known as type-level lambda. There are still restrictions on the arrows though... you might be right that putting an unmatchable arrow after a matchable one would never happen. It's all very moot now, though, so I don't think it's worth unpacking today. If you're curious about this, see my thesis, but I don't recall addressing this specific point in the text. You'd have to stare at the formalism to see if it's allowed... and good luck with that. :)

OK. Will revise proposal to get rid of the twiddlies.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Sep 14, 2017

The proposal is now revised. In the absence of further commentary, I'll submit for a decision in a few weeks.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Sep 15, 2017

Apologies for the tossing in a late objection, but something is nagging at me after reading the revised proposal. What will happen with respect to declarations like this one?

data Foo (k :: Type) :: k -> Type where
  MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)

This has a CUSK, as evidenced by the fact that you can write the polymorphically recursive type signature for MkFoo. But what happens after this proposal is adopted, and you now have to write a top-level kind signature for Foo in order to make it kind-check? The problem is that the kind of Foo is:

Foo :: forall k -> k -> Type

Where forall k -> is a visible, dependent quantifier. But you can't write this kind signature today! Does this mean that we would be unable to write the type signature for MkFoo now?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Sep 17, 2017

Oh dear. You're absolutely right, @RyanGlScott. I suppose I'll submit another proposal for introducing that syntax for kinds, upon which this one will have to depend.

@ezyang

This comment has been minimized.

ezyang commented Oct 12, 2017

The proposal notes that it's insufficient to specify a kind signature in an hs-boot file, because there is extra information you might need. I think this reasoning also applies to Backpack/hsig files (alas!)

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 14, 2017

I have filed #81 to fix the problem Ryan brought up a few comments ago. This proposal can be considered stalled until that one is accepted.

@RyanGlScott RyanGlScott referenced this pull request Oct 14, 2017

Closed

Deprecate -XTypeInType #82

@nomeata

This comment has been minimized.

Contributor

nomeata commented Nov 10, 2017

I’ll mark this as dormant to get it out of the list of proposals under discussion.

@nomeata nomeata added the dormant label Nov 10, 2017

@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

Hmm, maybe we need a separate label for proposals blocked on other proposals.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Feb 23, 2018

Please, let's not. Hopefully, that's a rarity. :)

Although, this is blocked by #81, which is pseudo-blocked by #102. Urgh.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Apr 16, 2018

With #102 successfully tabled and #81 under renewed committee consideration, I'd like to submit this to the committee as well. @nomeata

@nomeata nomeata requested a review from rleshchinskiy Apr 16, 2018

@nomeata nomeata removed the request for review from rleshchinskiy Apr 18, 2018

@AntC2 AntC2 referenced this pull request Jun 21, 2018

Open

Top-level signatures #148

@nomeata nomeata merged commit c69bb2e into ghc-proposals:master Sep 30, 2018

nomeata added a commit that referenced this pull request Sep 30, 2018

@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