Clarifying dependent types

#1

I just read the great write-up about dependent types in Bind the Gap: https://bindthegap.news/issues/BindTheGap-02Dec2020.pdf I’m grateful to the authors, @vrom911 and @ChShersh, for putting this together.

Given the controversy around dependent types, I want to go on record here to clarify a key point raised in that write-up. (Readers may also want to check out https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-736850050, which debunks these and other common misconceptions.)

  • There are no plans to remove punning from Haskell. That is, a definition like data T = T Int Bool will remain valid. Even with -XDependentTypes enabled. The challenge with punning (note that the example definition defines a type T and a constructor T) is that any mention of T is potentially confusing: do we mean the type or the term? So, with dependent types, it is awkward – but still always allowed – to use punning. At worst, with some combination of extensions, usage sites would have to disambiguate between the type T and the constructor T. But this would happen only with certain extensions on, and the disambiguation mechanism should be easy.

  • Similarly, there are no plans to change the meaning of [Int] in a type – at least, if no extensions are enabled. The bracket notation is, effectively, a pun, like the T in the bullet above. So, with, say, -XDependentTypes, the use of [Int] in a type might be ambiguous: do we mean the type of lists of Ints? Or do we mean a list of types with one element, Int? We would have to disambiguate. One way to do so would be using List Int to talk about the type of lists of Ints, and so https://github.com/ghc-proposals/ghc-proposals/pull/270 proposes a new module in the libraries shipped with GHC that will export a List type that means exactly that. Again: there are no changes here to any code that uses extensions that already exist.

Thanks again, @ChShersh and @vrom911, for drawing your attention – and ours, collectively – to dependent types, and for taking the significant amount of time in writing up our conversation. Incidentally, your little Settings example for dependent types is a nice, simple way of showing how dependent types can increase expressiveness. Thanks for including that.

11 Likes
#2

I use punning all the time, but I’m becoming increasingly leery of the practice because I’ve seen too many beginners confused by punned names. I didn’t appreciate this in the past because it wasn’t a problem for me personally, but teaching people Haskell and working with casual Haskellers on a work project showed me that it does add a cognitive burden for other people. Haskell being Haskell, we definitely don’t want to add any mental overhead we don’t have to!

At the same time, there often aren’t separate names that make sense (especially for newtypes), and conventions like MkFoo for constructors are really awkward. Honestly, I think this points to a small but real design flaw in Haskell: there is no clear connection between a type and its constructors, and we rely entirely on context to differentiate the two. Context is great for experienced users, but adds a real burden to beginners. A great analogy is the challenge of dealing with polysemy when teaching natural languages, which is an active area of education research.

Changing this is out of scope for Haskell work—that ship probably sailed before I was born :P—but I would carefully consider how to avoid this kind of pattern if I were designing a Haskell-like language today. I haven’t thought about this too much, but I’d probably go for something like Rust’s approach of namespacing constructor names with the type name, with some kind of syntax sugar to make pattern matching less visually redundant. This also has the advantage of letting multiple types with the same constructor name coexist peacefully, just like records with the same field name (ho ho).

From this perspective, having a syntactic way to disambiguate seems actively useful even without the context of dependent types. I don’t remember the exact syntax that’s been proposed, but if we had some extension where types and constructors looked a bit different ('Foo vs Foo or something), I’d seriously consider making that the default style for my own projects, backed up with a lint rule.

All this is to say that I don’t see this aspect as a downside of depdent Haskell at all :).

6 Likes
#3

The time I want punning most in my own code is when I have one constructor for a type. For example, if I have a newtype Age = ... Int, I don’t like being creative to fill in the .... The name isn’t all that helpful in gaining understanding – it’s the name of the type that’s important for understanding.

But other languages have solved this problem: they use new. That is, the constructor for type Foo in some languages (e.g. C++, Java) is spelled new Foo. Though I think we’d need a new keyword to pull it off (adapting, say, default for this seems a stretch), we could consider introducing that keyword into Haskell. We could also use the keyword in the definition:

newtype Age = new Age Int
-- or 
newtype Age where
  new Age :: Int -> Age

It’s a bit non-Haskelly. And it would make us look more like other languages. But it might make our code just a bit more perspicuous, and that’s good.

3 Likes
#4

Would there be any ambiguity in patterns?

Even if there isn’t, I’m not sure losing the clear syntactic relationship between constructors and patterns is a good idea overall.

1 Like
#5

Since the new HF ED’s experience in this matter has generated renewed interest:

serras:

We need to acknowledge that people are used to the dichotomy between values and types.

…or maybe even prefer their separation. But I have been wrong before, and maybe e.g. Ohmu was just “ahead of its time”.

From BTG 2020-12-02:

  • Overcoming Stereo types: Using type-level programming in Haskell to parse tricky JSON

  • [in the “Loco-motive” article]

    Dependent types exist for a while in other programming
    languages, for instance, Agda, Idris, Coq, etc. They are known to be used mostly in research areas (for writing proofs) or in verification systems where it is crucial to get everything correct (e.g. aeroplane software).

…did we choose the wrong paradigm - should we be using languages based on e.g. predicate logic instead of higher-order functions? At least then the difference between types and values would be much smaller: we could use Prolog for both.

#6

I’m curious what the state of DH on the GHC team is. From my perspective, it seems that DH simply has too much weight behind it to not be added eventually, but I am not clear on the timeline.

In Simon’s recent Haskell Interlude podcast, it seems he is still apprehensive about the choice: I am surprised by this seeming lack of cohesion. Some questions I feel like are not clearly answered:

  1. Are proposals being worked on to implement DH (specifically relevant types) in GHC?
  2. Is there still disagreement on the GHC team/wider ecosystem as a whole over DH?
  3. Nowadays I regularly hear Liquid Haskell as a suggested replacement for DH. Is this a direction being actively pursued? Do the directions conflict? Can they both be worked on simultaneously?

I hope I’m not stirring up drama - if there is rethinking happening it is no problem, but I personally would love to know. As an avid follower of the DH story, it would be great to have some sort of “DH status”, which I have seen hints of in the past (such as Richard + Simon’s private DH google doc). Perhaps something like the GHCJS implementation plan that I saw recently for IOG’s work…

#7

Lots of these questions can be clarified by reading the relevant GHC proposals, both accepted and in-discussion, particularly Design for Dependent Types but also others like Modern Scoped Type Variables.

#8

…or maybe just cautious:

  • from what I’ve seen of it, the official arrival of dependent types in Haskell would be “a turning point” for type systems, much like the inclusion of type classes all the way back in 1987. As every experienced Haskeller knows, there’s at least one problem with those which seems to elude a practical solution - the somewhat pejoratively-named “orphan instance” (of course, there are probably others). Who knows what new and equally-as-obstinate problems will appear if Haskell “goes dependent”…

  • At least one recent language arose from the frustration regarding the long build times for one older language in particular (IIRC, not Haskell; it’s more commonly categorised as being OO) as a result of its type system. There have already been some “memorable” complaints about this in Haskell builds - it would be unfortunate if dependent type aggravated matters further, to the point of people seriously contemplating an all-new nonstrict functional language without dependent types (and perhaps type classes!)

  • For better or worse, Simon Peyton Jones has ended up being “Mr Haskell” (the language, not the person) - if your name was equally as synonymous with an endeavour so widely-known, would you not be more than a little cautious about a similarly consequential change?

But these are just my opinions: let’s see what @simonpj says…

2 Likes
#9

I would describe myself as cautiously supportive of adding dependent types to Haskell. Let me say in a bit more detail what I mean by that.

  • A dependently typed language is not one well-defined thing. There is a huge design space, with many interesting tradeoffs. That is one reason for caution: in a language like Haskell that is used widely in production, it makes sense to make careful, incremental steps rather than that a big-bang jump to a destination that we may live to regret.

  • I am a passionate advocate of static type systems; as I often say, static types are by far the world’s most widely used and effective formal method. Haskell is a laboratory for exploring the bleeding edge of what you can do with static types, and I am proud of that.

    But a key feature of static types is that they are comprehensible to programmers. I think that is true today – but only just. A reason for caution is that we must not make Haskell so weirdly sophisticated that no one understands it any more.

    That said, there is one way in which adding dependent-type features arguably makes the language simpler, not more complicated, becuase terms and types become more alike. To take a different example, adding kind polymorphism was a complication in one way, but it made Haskell simpler in another: we can write polymorphic functions at the term level, so why can’t we do so at the type level?

    But the details of full-spectrum dependency are gnarly, and so again I am attracted by making incremental progress: adding features that may be inspired by the North Star of dependent types, but which each make sense individually, and improve the lives of programmers.

  • Speaking of a North Star, I was a co-author on A design for dependent types proposal, which has been accepted by the GHC steering committee, a decision that I supported. It lays out a design sketch for adding more dependency to Haskell. To quote: “This current proposal aims give some detail to what dependent types may look like. Acceptance does not commit us to an unalterable course of inclusion of exactly the features described here. But it would suggest that other proposals in this space should be designed in such a way that they are compatible with the details presented here.”

    So the specifics will be the subject of future, more detailed proposals, but we do have a public, agreed direction of travel.

  • As the proposal says explicitly in Section 4.11, I am not yet signed up to Glorious Vision of collapsing types and terms into a single level. I’m not definitely against it either, but I am not yet persuaded that the benefits would justify the costs. In particular, the costs to GHC’s implementation, which treats types and terms quite differently, would be very considerable. (This cost/benefit tradeoff might look very different in a language whose design, and compiler, embraced full spectrum dependency from Day 1.)

    Perhaps I will be persuaded in the future. For example, it took some time for Stephanie and Richard to persuade me that TypeInType was a good idea, but persuade me they did. For now, it’s an area of caution for me.

    Meanwhile, I think we will get huge value from debating, adopting, and implementing the earlier design changes sketched in A design for dependent types. Indeed we are well advanced along that path already.

  • I’m a big supporter of Liquid Haskell, and I’d love to see enough effort invested in it so that it can come “in the box” with GHC. But that’s a big job, and more people will need to get involved. Do join the effort!

Simon

8 Likes
#10

The caution you describe is fitting, particularly because there are so many unknowns, and the cost of reversing an implemented decision is not to be taken lightly. Similarly, given that much of the challenge of figuring this out requires significant experimentation and exploration, I think the thing that is most-often missing from the discussion around DH, is how to best “cushion” (or isolate) the experimental/exploratory future world of DH from day-to-day, non-experimental, production use of Haskell (and the ecosystem of packages/documentation/etc surrounding that). And to get this out of the way up front: while our language pragmas are great, wonderful, etc, I think there’s an argument to be made that they are not a sufficient enough cushion or mechanism, for isolating a multi-year “we’re trying to figure out what the best implementation looks like” from “we know this works well”. It’s been mentioned elsewhere by other people, but the solution is probably in the realm of some sort of LTS-type of social/technical agreement and implementation. Personally, I think that includes a standard lib/prelude and documentation. In other words, we need to define what pragmatic, correct, reliable Haskell looks like, and we need to allow space for “figuring out what we don’t know about DH”, isolated in such a way that you can get in and dirty if you want to, but aren’t pulled into the muck if you’re looking to stick with what’s agreed as “fit for production”. When we’re ready to call DH “production-ready”, we flip the switch / bump the LTS along with the docs, standard lib, packages, etc. I think it is a challenge to figure out what that looks and feels like, but given what’s at stake, it’s not a challenge to shy away from.

#11

:The surface syntax proposals for DH are largely finished, so per Wadler’s law I am hoping progress can pick up speed again :).

The most important parts of the DH work should be the most uncontroversial: current kludges like type families have very terrible semantics making them extremely frustrating to use, and whether or not they become just functions or not it would be prudent to:

  1. Reimplement them with better semantics
  2. Share underlying notions / implementation of partial evaluation between optimizer and type checker.

Greenspun's tenth rule - Wikipedia is

Any sufficiently complicated C or Fortran program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp.

I would argue we are in a very analogous situation where

Any implementation of a sufficiently complicated piecemeal generalization of Haskell contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Dependent Haskell.

So the really important thing is to fix that: GHC Haskell is a nice enough language but GHC the implementation not in a healthy state as far as its software engineering is concerned! A strong effort to shore up the internals of GHC should be an excellent approach to avoiding bike-shed controversy, and get us closer to Dependent Haskell purely as a side effect!

5 Likes
#12

I’m glad to see this is recognized.

My doubts about DH aren’t so much about the features itself or the implementation cost. They are rather practical: what will people do with it?

I’m a big fan of F*, which does have dependent types… but is also a rather specialized language for specific use cases. Additionally, it allows to extract F# code. For a language that has such a specific use case and transpiles to something else, there’s less caution to be had.

For Haskell, I’m specifically wondering about:

  • if depedent types will eventually be used in base, what effect will this have on newcomers?
  • will I be exposed to type-spaghetti in every second library? What will this do to APIs?

I think these questions are really hard to answer and I understand they are probably not much considered when designing DH, because it’s really difficult to say.

That said, I’m much more a fan of liquidhaskell or the idea to just write a superset language of Haskell that transpiles back to it. Those things are clean and totally opt-in. Once this lands in Haskell proper, it will no longer be opt-in, even if it’s behind a language pragma.

The challenge with sequential incremental steps is that it may never lead to a satisfying design as a whole.

3 Likes
Haskell plush toy
#13

This is interesting to hear. Could you expand on that? (Perhaps the best place would be a Discussion on the ghc-proposals repo.)

1 Like
#14

@tomjaguarpaw I wish I had a better thing for you to read squarely on this topic, but for now I might recommend this reply from @hsyl20 Back-end responsibilities are distributed throughout the compiler (#20927) · Issues · Glasgow Haskell Compiler / GHC · GitLab on a more narrow issue that nevertheless discusses large issues. This isn’t terribly near the Dependent Types side of things, but conversely discusses violations of what most Haskellers (and even not Haskellers) think is good software engineering that are more flagrant / clear-cut.

For me, the grand narrative here is basically what one gets from synthesizing the patches and writings of @hsyl20, and @int-index (in addition to @rae).

  • We can work from the bottom looking at the code, ignoring what it is supposed to / trying to do (i.e. the language itself) and work our way up.

  • We can also work our way from the top down asking why aren’t “Milner’s coincidences” and dustier corners of the language broken up so we have fewer, more orthogonal features.

I really believe at best this is all the same fight and goals: expressive power is never the goal but the icing on the cake one gets as a result for pushing for modularity and compositionality.

The right thing to do is bring more attention to whatever approach ought to be uncontroversial with enough scrutiny. DH is, as I said, hopefully about to get less controversial as we escape the clutches of Wadler’s law. But the awkwardness of internals of GHC as described by @hsyl20 should be even less controversial if only people new. The challenge is a survivorship bias where:

  • Most Haskellers of course just use GHC as a black box.

  • Perhaps large “silent” group of Haskellers try messing around with the GHC API a few times, but are frustrated by its poor shape. Perhaps they think “surely it doesn’t need to be this bad”, or perhaps they merely internalize “compilers are hard” and think the problem is their own skills and not the hostile interface.

  • Those that stick around working on GHC tend to spend a very large portion of their time working on GHC and not other projects. Whether they never minded these issues to begin with, or gradually become accustomed to these issues (and unaccustomed to how things are done “elsewhere”) is besides the point.

6 Likes
#15

Lastly, I do believe that the implementation details of GHC to subtly but profoundly shape the “Overton Window” of library, language, and other “ecosystem” design decisions. I suppose this belief is implicit in all my comments, but I think it is good to spell out explicitly.

For this reason, I think folks that are perfectly happy just using GHC as a block box executable (and therefore not directly caring about how it is implemented in the slightest) still should care about the state of things “under the hood”. The state of things will come back to affect the issues you all do in fact directly care about by influencing their Overton Window.

#16

I think it would be a great service to the community if you could write all these details up into an article. It’s great that you have perceived them, but of much greater benefit to the community if you can share them!

2 Likes
#17

Yeah I hope that will happen too! Hopefully I can merely co-author :).

#18

I honestly do not understand the type spaghetti argument.
Dependent Haskell would likely reduce existing type spaghetti in libraries, by e.g. allowing partial application of functions at the type-level. I don’t see how making types easier to manipulate will mean that abstractions that are possible now will instead be implemented in an overly complex manner.
However, I do think that we will see complex abstractions that simply weren’t possible before.

2 Likes
#19

(code/type) spaghetti isn’t a result of lack of expressivity. It’s the opposite.

This is as much a social experiment as it’s a technical one, but I hear only discussions about the latter.

Quoting from https://artandlogic.com/2021/08/exploring-dependent-types-in-idris

As the code that you’re formally verifying becomes more complex, implementation quickly goes from easy, to time-consuming, to an active research area.

We’re creating a new language, incrementally, that will not be anything like what Haskell was, if it succeeds. Maybe that’s good, maybe it’s not. That will depend on the users of the language. Who will buy into it? How will they use it?

This has never been done before in a mainstream language, has it? Yes, I consider Haskell mainstream.

Many Haskellers can barely keep up with all the tools that we already have, see Stephen Diehl’s great compilation.

Dependent types being entirely opt-in would solve this issue. But again: a language pragma is not opt-in. I’m not saying I know what’s best, I’m just raising these concerns.

1 Like
#20

@hasufell your arguments make sense to me in the abstract, but do not fit the facts as I see them.

We’re creating a new language, incrementally, that will not be anything like what Haskell was, if it succeeds. Maybe that’s good, maybe it’s not. That will depend on the users of the language. Who will buy into it? How will they use it?

No, that is what we’ve been doing the past 10-20 years. The current hodge-podge of features vaguely gesticulating in a Dependent Haskell direction. The direction of gesticulating is not the problem. The hodge-podge doing the vague gesticulating is.

This has never been done before in a mainstream language, has it? Yes, I consider Haskell mainstream.

C++11 made a lot of new stuff. The ickiness vs something like Rust was that there was no stomach for getting rid of bad old stuff. We thankfully don’t need to get rid of anything! Certainly not in Haskell 2010. I would advocate getting rid of type families, but this is purely optional; we can support them along-side the better alternative indefinitely.

Many Haskellers can barely keep up with all the tools that we already have, see Stephen Diehl’s great compilation.

That’s because we have the hodge-podge. Once we unify the current mess into Dependent Haskell, it will make more sense not less!

Dependent types being entirely opt-in would solve this issue. But again: a language pragma is not opt-in. I’m not saying I know what’s best, I’m just raising these concerns.

On a technical level it sure is opt-in. You mean on a social level? Sure, but we already have that problem today with the hodge-podge. If we have that problem regardless, I don’t see this as an argument not clean things up.

2 Likes