[ghc-steering-committee] Recommendation for #378: support the design for dependent types

[Joachim Breitner]

Dear Committee,

> Richard has now revised the “Design for Dependent Types” proposal,
and has resubmitted it. 

I am in support of this proposal. I expect it will be painful at times
to go that route, and it will creak at the edges, but my sense is that
this eventual unification of types and terms is something that will
become something we’d expect from a “modern language”, a bit like we
expect function types and lambdas these days, and I have some hope that
eventually, in a relatively far away future, Haskell will nicer and
simpler because of this 

The alternative, sticking to a non-dependent design (and yes, getting
some benefits from that too), could lead to Haskell becoming a
“language of the 00s”. Useful, mature, great to get work done, still
something that not everybody knows and you can still feel a bit special
for knowing it. But no longer the language that is _both_ productively
usable and at the same time incorporates new, research-close features.
It might become a bit like Perl in that sense. (Ok, that’s a bit too gloomy … take it as hyperbole).


I expect that discouraging punning will be maybe the most painful
part of that route, for the wider community.
  import GHC.Tupe; swap ::
Tuple [a,b] -> Tuple [b,a]
just isn’t as smooth as `swap :: (a,b) ->
(b,a)`.
(And we can’t even cargo-cult from the ML family and use
`(a * b) -> (b * a)` for the type of types…)
I acknowledge that, I wish
there was a better solution, but what’s in #378 seems to be the least
bad.


I am amused that this proposal rests on a PEP, and happy to see that
the LSP gets a more central role in the language design ;-)

Cheers,
Joachim


PS: Quick note about #291 (type variables in patterns), just to record
my current thinking: 

I understand the reasoning, it would be nice to
treat a `@(Maybe a)` argument like a `(Just x)` argument in patterns,
binding `a`. But I am not convinced we can afford to toss out the
ability to use an _occurence_ of a type `a`. My interpretation of
#378’s implication on #291 is that we’ll have to find a way to
distinguish binders from ocurrences that works independently of types
and values (I believe we do need it for types, and I think we should
have this for values as well anyways, as PatternSynonyms _should_ be
able to abstract over patterns that have _required_ values, not just
required constraints.)

-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/