Clarifying dependent types

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.

7 Likes

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 :).

2 Likes

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.

1 Like