Clarifying dependent types

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