Thoughts on future additions of type-level features

Change Proposals
#1

There are a number of type system features which Haskell has and PureScript currently doesn’t, and which some people might want to see in PureScript one day. For example:

Note that some of these are subsumed by others, eg GADTs subsume existential types.

I am beginning to feel that it may be worth clarifying a stance on whether or not we want PureScript to get these features, that is, distinguishing “we do not want to add this because of reasons X, Y, Z” from “this would be nice to have but we just haven’t gotten around to it yet.”

Firstly, I want to draw attention to the fact that we do not have anywhere near the resources or expertise that GHC does for implementing and maintaining these kinds of features (or at least, this is my impression). For example, there is a long standing bug in kind unification which we haven’t yet gotten around to fixing.

Because of this, I would like us to be much more conservative about adding type level features than, say, GHC Haskell is. Any big type level feature is probably not only a fair bit of effort to implement in the first place, but also potentially a large maintenance burden, especially if, say, a few months after initial release, we find a serious bug in a feature which we struggle to fix but cannot remove because a chunk of the ecosystem has come to rely on it.

I also think there’s a lot to be said for having a smaller language with fewer features: the more features there are, the more you need to learn if you want to make the best use of the ecosystem, the more scope there is for those features to interact poorly with each other, and the more effort is going to be required to specify the language (if we ever get around to that).

I think a particularly convincing example of the utility of ruling out some particular type system feature is when that allows library authors to make stronger assumptions about what can safely be done. For example, all type constructors in PureScript are injective; this allows library authors to safely provide functions such as lowerLeibniz. As I understand it, adding type families would invalidate this reasoning.

So hopefully you can now see where I’m coming from when I say I’d like to start ruling out type system features.

In particular, since we have an open PR implementing Coercible, I think now would be a good opportunity to raise the possibility of committing to not adding type families. Also, if we want to implement existential types, I think we should commit to not adding GADTs, since GADTs subsume existential types; if we had both GADTs and existential types, we’d have two different and probably incompatible ways of doing the exact same thing.

What do you all think? Does this all sound sensible or am I missing something?

Some other relevant posts (both by @paf31, as it happens) which have helped shape my thoughts here:

14 Likes
Get row from record type alias
What does injectivity of type constructors mean?
#2

So you vote for no on type families. And the reason is that it is incompatible with other not-yet-built type system features. Any opinions on that one, specifically?

#3

Pretty much, yes, although I’m not sure I’d go as far as ‘incompatible’, since I think Haskell has everything on the above list. It’s more that I think it’s a bit more difficult to have all of these features work nicely together.

#4

Would it be helpful to choose features based on the types of practical things they would enable? It’s been said that PureScript wants to only add features which are practical, rather than prematurely adding “academic” features.

I imagine these features are “basic” enough that there’s numerous things that can be done with them. Maybe we want to judge the practical things these features enable by “is it an order of magnitude better than the alternative way of writing them?”

I really like having the ability to be more expressive in my type-level expressions, FWIW. I’m trying to find ways to kick-start the conversation here, or take it in baby-steps in a productive direction.

#5

I imagine this thread should avoid discussing more radical changes to the type-system to get the expressive abilities enabled by some of the type system features mentioned, yeah? Such as the Idris-style type system, which I hear has supremely expressive types.

I only bring this up to scope this thread and to pre-emptively answer that question. A radical change like that would likely be a syntax/semantics breaking change, so that would surely be a PureScript of a different name (e.g. PureScript2 or ReallyGoodScript). I believe this thread is about the “incremental” type system improvements, whereas the more radical changes would be separate discussion.

#6

Would it be helpful to choose features based on the types of practical things they would enable? It’s been said that PureScript wants to only add features which are practical, rather than prematurely adding “academic” features.

I think the idea that some features are “practical” and others “academic” is a bit of a red herring; my impression is that PLT academia does actually care about most of the same things I do as an industry software engineer. If a feature seems academic it might just be because the person who wrote about it didn’t manage to come up with a convincing practical example at first; I’m sure lots of people consider monads academic.

With that said, I would definitely agree that any feature we might want to add needs to have a number of motivating examples which are easy to express in the presence of said feature, and also difficult in its absence.

I imagine this thread should avoid discussing more radical changes to the type-system to get the expressive abilities enabled by some of the type system features mentioned, yeah? Such as the Idris-style type system, which I hear has supremely expressive types.

I think this thread is perfect for discussing bigger features than the ones I listed! But also, I think anything truly radical (such as proper dependent types) is very unlikely to happen. Even if someone did put together a viable proposal and an implementation, I’d probably still be against making that kind of change. It takes us in precisely the opposite direction which I’d like to see the language moving in, that is, of becoming more stable (cf Phil’s “the state of things” post).

I already mentioned some thoughts I had about dependent types on the Pi types proposal, and I think the same argument would apply for any radical type system change:

if a language is going to have dependent types, I think it should probably be designed from the start to have them. If you wait until you have a large ecosystem, set of principles for what is idiomatic and which features are appropriate to use in which situations and so on, and only then try to add DTs, you may well end up with an awkward design, because (at least if you look at Idris and how its standard library and ecosystem diverges from ours) it seems that dependent types have big implications for all of these things.

2 Likes
#7

Copying my thoughts from elsewhere on this:

From this list, things I would be very sad if we never implemented:

  • existentials (if we’re not going to have GADTs)
  • polykinds

Thing I would like a great deal:

  • Coercible
  • DerivingVia

I would love to have GADTs too, but I also have worries about the complexity of implementation. There is a follow up paper to the “complete and easy” paper that our type system is based on, but since I find the first one pretty unreadable, I don’t imagine I’ll have much luck with the second one either.

Type families allow for some amazing stuff, but they’re such a large topic that I’m only familiar with elements of, that I don’t even feel qualified to give an opinion on how difficult it would be to integrate or maintain them. I think we’ve actually already solved some of the issues, in that I know part of their implementation difficulty is similar to that of functional dependencies. If I had to give an answer either way I’d probably vote for ruling them out for the foreseeable future.

I know even less about using constraint kinds than I do about type families. We already did a bunch of work laying the foundations for their inclusion (no tupled class constraints for members, etc.) but I don’t have any strong feelings either way about them. I might do if I knew of a case where constraint kinds would save me :smile:

I don’t really understand the Pi types proposal, so also no strong opinion there. It seems a lot weirder to me than “visible dependent quantification”, despite the unfortunate forall k -> syntax in Haskell. I would like some solution to “the proxy/type applications problem” though, and it seems relevant to polykinds too, since some of the concerns there when we started looking into it was around how to quantify.

Maybe we should add QuantifiedConstraints to the list too, that’s something else in the “things I would like a great deal” category.

And from Nate:

https://www.cl.cam.ac.uk/~nk480/gadt.pdf is the GADT paper, FWIW. I don’t know if I’d say our type system is based on the original complete and easy paper other than bidirectionality, and maybe inspiration for handling higher-rank stuff… It’s main contribution was a novel alternative to skolem machinery, which we certainly don’t implement.

2 Likes
#8

I would like constraint kinds since it would make variant a lot more useful, but it wouldn’t be very nice to use without at least existentials.

data Dict c = c => Dict
2 Likes
#9

I very much agree that it is important to think about a coherent set of (type level) features for PureScript. This will not only result in a smaller and easier to understand compiler, but also in more best practices for the language and less fragmentation (think functional dependencies vs type families in the Haskell community). We should find the right balance between power, simplicity, and maintainability.

TL;DR: add existentials and polish the existing type system focussing on higher kinded types, user defined kinds, constraints, row types and rank-n types. Most type level features programmers are asking for are already there but need some polish!

I think most of the functionality programmers ask for in PureScript, can be emulated with existing features or by extending and polishing existing features. GADTs, type families, and pi-types are things that are new for PureScript and do not naturally fit into the existing future set. Therefore, I would only vote for adding existentials and then put effort in polishing existing features like the kind system, constraints solving, and deriveability.

The addition of existentials is minor. Combined with already existing features like multi parameter type classes and functional dependencies, would give us most of the power of GADTs. These kind of data types are called Extended Algebraic Data Types, as discussed in this issue. A naive implementation would carry dictionaries with type equalities, but maybe this could be optimized away. Most of it is already possible in PureScript using rank-n-types, but real existentials and dictionary packaging are way easier than unwrapping foralls by hand.

With functional dependencies we can already do a lot of type level programming. The thing is fundeps are relational and do not have a nice functional syntax. However, I think this is a solvable problem. Adding some kind of syntax to give the feeling of associated types, like proposed by Phil not so long ago. This would be enough for most uses cases. As Lennart Augustsson put it, typefams grew out of the desire to use associated types. Mark Jones already noted the features between fundeps and typefams are quite similar and that most can be done by adding some syntactic sugar. No new features are needed and the type system theory can stay the same.

When we would add typefams, we will have two different ways of doing the same thing. But we already invested into on of them! And once you have them, you’d probably like injectivity annotations for type families. But with fundeps you can already have bijective relations. Closed typefams give you more power. But this is exactly what instance chains do. And so on…

Streamlining the kind system would make it possible to easier declare user-defined kinds and type constructors on other kinds than Type. It is already possible to declare a new kind with foreign import, but a type constructor taking a parameter of some new kind is not possible. There is some strange separation between what you can define using a normal data declaration on one hand and using foreign data declarations:

foreign import kind Nat

foreign import data Z :: Nat  -- Ok
foreign import data S (n :: Nat) :: Nat  -- Syntax error!

data Z :: Nat  -- Syntax error!
data S (n :: Nat)  -- Ok

The usage of import foreign kind/data declarations is a bit clumsy in my view. Why not stripping the import foreign, add a kind keyword and allow empty data declarations with kind annotations?

In the same line of polish, Constraint would be a build in kind and type operators like => would be appropriately kinded to allow them in the right places. Kind polymorphism would be something for a PureScript 2.0 release instead of 1.0, I think that will take more work…

2 Likes
#10

I’m certainly in favor of fewer big changes to the type system, as I’ve said in the past. As others have noted, there really aren’t many things which are absolutely necessary as opposed to just nice-to-haves. I don’t find myself reaching for type families at work, for example, since I have MPTCs with fundeps. I can count on one hand the number of times I’ve wanted GADTs over the course of about four years, and in those few cases, I was able to find a GADT-less solution. Not to say those things wouldn’t be nice to have, but I don’t think they are worth it when you consider the maintenance burden incurred.

Existential types is another one where I can get by easily enough with what’s available now. They seem easy, but they’re probably not, since you need new syntax for a place to hang the introduction of a new skolem variable.

Also, I know it’s almost laughable, but I would still really like to see what things would be like without the kind checker enabled. On the one hand, you can define more things (you get the expressivity of polykinds, plus rank-n-kinds, etc.), but at the expense of termination checking and error message quality when things go wrong.

#11

I’m sticking with this language regardless of which direction it goes. However, just speaking hypothetically here, but to satisfy those who want to go a different direction than those that the language developers ultimately take here, would language extensions ever be considered?

I’d rather not follow Haskell in that way, but I thought I’d bring it up.

#12

About taking out kinds - would that mean “no kinds”? Or just “no kind checking/unification”? I ask because IIRC there’s several kinda-neat PureScript libraries which make use of kind-level stuff. I don’t mean to say those libraries must absolutely be supported, just that kinds enable fun things.

Regarding an alternative to “kinds”, I’ve heard about a “universe” system. I don’t know if it’s possible to fit “universes” into PureScript, but if there’s interest in removing kinds to gain more kind-level expressivity, what do people thing about universes? I don’t know if universes are even possible in PureScript.

#13

I’d really prefer not to add language extensions; if we have n extensions, assuming they’re all able to be turned on and off independently, then we have 2^n different versions of the language, and that becomes very difficult to work with very quickly as n increases.

1 Like
#14

Thanks for the clarification! I’m glad.

#15

I noticed just now that purescript does not support orphan instances; is this by design or just a missing feature? I can understand they might cause compile-time conflicts, but this seems to be outweighed by the flexibility of being able to prove an object implements a given interface without having to create an explicit wrapper.

2 Likes
#16

It’s by design, they became explicitly disallowed sometime in 2015.

#17

I still really like the idea of your “dynamically kinded types” idea Phil. Would bring in a lot of power. It’s really worth an experiment!

#18

IIRC you get universes in a dependently typed setting. It would mean flattening out the levels of terms, types, kinds, sorts, etc into one language. You need to carefully think about totality, as functions could be applied on the type level during compilation.

PureScript’s type system is largely based in Haskell’s (with some extensions). Going in the direction of universes would imply a language with a radically different type system than we have now.

1 Like
#19

Dynamically kinded types sounds neat but I’m hesitant to implement anything which hasn’t had some level of study by academia; are there any papers covering this idea?

#20

Not that I’m aware of… Would be an experiment of how to implement kind polymorphism in a different way.

I’d love to research this idea more but I’m afraid I won’t have time for it during my PhD.