Should higher kinds still be behind a language import?

Language Design
1

SIP 18 (SIP: Modularizing Language Features - Google Docs) introduced language imports, and gating higher kinds behind the import language.higherKinds was part of that SIP.

The rationale at the time was

Why control it? Higher kinded types in Scala lead to a Turing-complete type system, where compiler termination is no longer guaranteed. They tend to be useful mostly for type-level computation and for a relatively narrow set of highly generic design patterns. The level of abstraction implied by these design patterns is often a barrier to understanding for newcomers to a Scala codebase. Some syntactic aspects of higher-kinded types are hard to understand for the uninitiated and type inference is less effective for them than for normal types. Because we are not completely happy with them yet, it is possible that some aspects of higher-kinded types will change in future versions of Scala. See my post “Scala - A Roadmap” to scala-language for details. So an explicit enabling also serves as a warning that code involving higher-kinded types might have to be revised in the future.

This reasoning is still preserved in the doc comment.

I’d like to discuss whether the rationale presented is still applicable, whether there are other reasons to have the feature behind a flag, and if higher kinds could be enabled without a flag.

Pulling the reasons apart, we have

  • Compiler termination is not guaranteed
  • The applicability is relatively narrow
  • Using HKTs is a barrier of entry to newcomers in a code base
  • Type inference is less effective
  • It is possible that details may change in the future

With cats-effect and fs2 quickly gaining traction, HKTs are quickly becoming more common in my own scala projects. This makes the second point weaker.

While I agree using HKTs is a barrier of entry to newcomers in a code base, I suspect this warning is rarely heeded. It doesn’t seem to me that many code bases choice to (not) use HKTs is triggered by the warning on this import, and I don’t think this warning helps with that.

-Ypartial-unification eliminates important issues with inference, and Partial unification unconditional; deprecate -Xexperimental by milessabin · Pull Request #6309 · scala/scala · GitHub while not yet merged seems to be a (wonderful) formality at this point.

As far as I know, the final comment about changing HKT semantics in the (indeterminite) future isn’t applicable anymore.

All in all, I believe it’s rare that people accidentally use HKTs, and possibly even rarer that this warning saves someones programmatic bacon. With the evolution of scala itself and the scala ecosystem, I don’t think it’s needed anymore. Is it maybe time to enable HKTs by default?

6 Likes
2

I think this is an interesting idea we should consider. As far as I see, a change of such a magnitude will require a SIP. Would you be willing to write one @martijnhoekstra?

3

If this discussion shows enough interest in the proposal to make it plausible it could pass as a SIP, I don’t mind going through the process.

1 Like
4

For me a barrier to understanding for newcomers to a Scala codebase, is actually the opposite. A new user can understand the concept of HKT more easily by looking at code, than trying that code and failing because of a missing flag. Once a feature is stable enough for a long enough period of time, I don’t think it should stay behind a flag.

1 Like
5

I don’t think they should be behind an import. HKT is one of the main advantages of scala over kotlin, in my opinion.

I don’t think we should discourage their use, which when applicable, gives really great abstraction power.

1 Like
6

Well, there are still open questions about that point, because we don’t have a soundness proof that handles higher kinds, and one is not trivial. I’m not sure what the consequences on language pragmatics should be, but “features of unclear soundness are experimental” sounds reasonable.

Of course, Scala has tons of features not covered directly by soundness proofs, but experts have some experience in distinguishing which features are “boring” extensions (which you could prove sound if some mathematician had unlimited time to spend on doing such proofs) and which proofs are instead non-trivial. And proofs involving higher kinds aren’t trivial; Sandro Stucki’s PhD thesis (Higher-Order Subtyping with Type Intervals · Sandro Stucki) is highly relevant, in that he studies a small extension of standard systems with higher kinds towards higher-kinded DOT, and the resulting proof is not trivial.

More in detail, Reducing open types is potentially unsafe · Issue #2771 · lampepfl/dotty · GitHub and IndexOutOfBoundsException when attempting to reduce ill-kinded types · Issue #2887 · lampepfl/dotty · GitHub are relevant. One of my first question to Martin was about plans on this; he has some ideas of what might fix that particular issue, but we don’t know what’s needed for a soundness proof, and how different would the semantics be. (Also note, that issue is not a violation of type soundness, but only of kind soundness when reducing open types in the typechecker; relying on kind soundness is an engineering decision that simplifies the type checker, but giving a type error if reducing a type violates kind soundness is an option that preserves type soundness).

My current (semi-educated) guess is that most real-world usage, especially Haskell-style usage (say, in cats) would remain unaffected by any changes. Currently, issues such as that one seem to arise from the combination of higher kinds and subtyping (in particular, as usual, using upper and lower bounds, which is the bane of DOT soundness proofs).

On timelines

Some people might ask about timelines. That’s a valid question, so let me answer right away: as a colleague said, you can give time estimates for some work if and only if it is not research, because research is about discovering actually new things, not about implementing ideas we have some understand of. And a soundness proof for higher-kinds in Scala is clearly research.

Should you be afraid of higher-kinds because of what I wrote? No!

Before what I wrote is misinterpreted: Tons of facts are true even if we don’t know how to prove them, and again, we haven’t discovered soundness issues with higher kinds in Dotty. Usage in cats found no soundness issues. OTOH, if you use them in original ways, we don’t have a proof you won’t find tricky issues.

FAQ on ongoing work

Here’s a short Q/A session.

  • Is anybody working on such soundness proofs? Yes.
  • Do the attempts have a chance? Hard to tell until the proofs are done.
  • How long will they take? Who knows.

Why are you writing to tell us “we have no clue”?

Because it’s hard to keep you posted otherwise. There’s a natural bias to say nothing till you’re done, and the outside community only sees no info at all. As an outsider I’ve had that feeling, like many others; so now as an insider, I’m trying (a bit) something else — even though the above is mostly a summary of info that is technically public (though probably hard to find and collect). But to be clear, this is just my perspective, not some sort of official statement.

Any (constructive) feedback is welcome, especially on the information sharing.

7 Likes
7

Can we put null behind a feature flag, then? It’s been proven to be unsound :stuck_out_tongue:

Seriously though, that’d be a good way to make it clear to beginners that working with null is not idiomatic in Scala. Perhaps the warning should extend to those cases where nulls might be observed even without explicit use (eg: tricky initializers).

8 Likes
8

Good point, that’s a policy I made up on the spot, not a real enforced one, and enforcing it would be hard. My main point was that higher-kinds semantics could still change; even more generally, the decision’s clearly not mine, I just point out information relevant to the decision.

On null, IIUC there are hopes of handling it in a more systematic way (though I haven’t studied this in too much depth), but there are multiple open research questions. Maybe we should add a temporary solution, and then only replace it when and if we find a better solution (and I’m not sarcastic). After all, if people want to keep using null (even temporarily), adding -language:null isn’t too much effort.

I think the major issue is not making the transition from Java too hard, but this is a warning, and most likely novices either don’t turn warnings into errors or can add -language:null.

9

IMO it would be a good idea to have null (as well as return, asInstanceOf, and maybe even (uninitialized) var) under language flags as advanced features that are nevertheless useful in some cases.

But that’s not this proposal (and a fight that I’m not inclined to take on).

I think @Blaisorblade intends to say (though I don’t want to speak for him, so please do correct me if I’m misinterpreting) that at least the last point - HKTs as we know them now in Scala are prone to future change - is at least somewhat justified by them being not proven sound, and new insights into their soundness might lead to changes to them.

However, while I appreciate the sentiment that HKTs are of inherent experimental status, it doesn’t seem to me that we should expect changes to the scala interpretation any time soon/on the 2.x timeline. If I’m mistaken on this point, that would be a pretty strong argument to keep them under a language import, so if there is sound the objection horns.

Yet they are not treated as experimental at the moment, and their experimental status is not a stated rationale of having them under a language import. It’s a good point to take along in the discussion, but it’s not IMO the final arbiter of whether or not a language import should be required for it.

1 Like
10

@martijnhoekstra you’re correct, in particular on:

Indeed, didn’t mean to imply otherwise or to correct you on the other points — hence “I’m not sure what the consequences on language pragmatics should be”. I do suspect Martin might care a lot.

Also:

However, while I appreciate the sentiment that HKTs are of inherent experimental status, it doesn’t seem to me that we should expect changes to the scala interpretation any time soon/on the 2.x timeline

Maybe SIP-18 was premature, but one goal was to ease transition to Dotty/3.x, which will be there “soon” (for some value of soon), and the rationale of the import was to inform users about potential changes.

Again, of course, please weigh this with the other arguments as you find appropriate :slight_smile:

11

@jvican WDYT, does this seem ready for a pre-SIP thread?

12

I think so. Something brief explaining the rationale and pointing to examples that show how often this feature is used will be valuable for the SIP too.