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 typeT
and a constructorT
) is that any mention ofT
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 typeT
and the constructorT
. 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 theT
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 ofInt
s? Or do we mean a list of types with one element,Int
? We would have to disambiguate. One way to do so would be usingList Int
to talk about the type of lists ofInt
s, and so https://github.com/ghc-proposals/ghc-proposals/pull/270 proposes a new module in the libraries shipped with GHC that will export aList
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.