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 Boolwill remain valid. Even with
-XDependentTypesenabled. The challenge with punning (note that the example definition defines a type
Tand a constructor
T) is that any mention of
Tis 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
Tand 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
Tin 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 Intto 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
Listtype 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.