I highlighted David’s perspective from HF in the original post for future references, I think that was great and informative for everyone.
If anyone could make another summary from community perspective so far from the discussions that’d be good to included too. Not sure where the conversation is leading to now otherwise…
There is no single “community perspective”, as this thread shows - you may need to be more specific as to what you’re trying to ascertain…
I do not understand this thread, had haskell ever been alive enough to allow 2 implementations? I am sure significant workforce needs to be continuously put into for each implementation. I doubt haskell community has enough manpower/resources for this anyway.
This is false.
Companies like meta, IOG or SCB for sure have the resources. They just don’t see enough of an argument to invest in that.
GHC is not maintained by volunteers alone. The primary maintainers are paid. The company they work for gets funding.
Not that I can speak with any authority on Haskell implementations in general, but what about Frege in particular? It for sure cannot compete with GHC, but I don’t think it is abandoned.
From that link, Frege can’t even compete with Hugs 2006: it implements (most of) the H98 standard; no MultiParamTypeClasses; so no FunDeps; neither (presumably) Type Families.
If it’s not abandoned, they’ve still a heck of a lot of work to catch up.
Note both MPTCs and FunDeps, also Overlapping Instances were supported in both GHC and Hugs by 1998 - but they were very experimental. They’d matured by 2006; but the two platforms had drifted apart; Hugs has some serious limitations but is robust as far as it goes; GHC still has nasty corners.
For a different approach to those nasties, there’s Habit – which is kinda the continuation of Hugs. (I’d say they’re also continuing ‘avoid success at all costs’.)
Also purescript deserves honorable mention.
Yeah. I was going to say there’s now a ‘big money corporate’ perspective that’s driving 9.x with performance and low-level features. But that doesn’t explain the corporatists here who are ‘stuck’ at 8.10.
The abstract research community/Dependant Haskell has gone to where?
I believe (and that’s my personal perspective) that Haskell has given much to the PL research community and has reached the bottom of the feature fountain. Nowadays, exciting new languages / research platform seem to be more oriented towards a mix of proof assistant and general-purpose language (Idris, Lean, Coq, Agda). The 2020 decade might be the one where we cement our legacy and bring it to the wider public, and leave the cutting-edge research to other languages that can innovate in more radical ways without hurting their user base too much.
Edit: Since agda2hs appeared in the landscape, I have been toying with the idea of having a mix of Haskell and Agda code in my systems, but ultimately running Haskell programs in which some parts would have been generated from Agda. But I don’t believe we should invest any resource to make Haskell a dependently-typed language for the masses at this point.
I don’t believe we should invest any resource to make Haskell a dependently-typed language for the masses at this point.
I’m not sure who you include in this use of “we”, but the company I currently work at—Serokell—is investing resources in exactly that. To be more precise, the form in which they are investing is paying my salary, as implementing dependent types in Haskell is basically my job. I would like to ask you not to try to change their minds about this.
Besides, the GHC Steering Committee has accepted the Design for Dependent Types proposal. There’s huge demand for dependent types in Haskell (there’s also some resistance, but it doesn’t cancel out the demand).
I don’t think I was aware that you were working on this topic. 
Is there a focus on the ergonomics of the system, or just an implementation? Is there a roadmap that can be read somewhere, or is the design proposal your roadmap?
Ergonomics are the entire point of the initiative.
We already have a way to model dependent types in Haskell using a combination of defunctionalized type families, data type promotion, GADTs, kind polymorphism, singleton types, etc. But this encoding incurs a heavy cost—both in terms of performance and in terms of ergonomics. My goal is to lower that cost as much as possible by adding direct support for dependent types to the language.
There’s no roadmap per se: instead of a specific sequence of steps we have a vision for the final destination and a bunch of ideas how to get there. Each step goes through the GHC Steering Committee to ensure its quality and that there is demand for it in the community. The nearest milestone is implementing the accepted GHC Proposal #281 “Visible forall in types of terms”. Then we will see where to go from there.
Fantastic then, I would be delighted to have my opinion changed with your work
When it comes to these sort of things I feel people only see the language part of the problem.
Ergonomics are not simply technical properties of a language. As the ecosystem adopts strategies and tools, ergonomics become an emergent property of how people understand (or don’t understand) a certain feature.
The design space of DT is so huge that I believe there’s no non-research language that has proven that it works well across an entire ecosystem.
This is another of those points where having two different compilers may be reasonable. And as a result keep DT out of the language spec and opt-in. But it doesn’t seem we are going that route.
Haskell was originally a consolidation of efforts from multiple statically typed lazy functional languages. There were once implementations such as Hugs, NHC from York, and UHC from Utrecht in addition to GHC. The Haskell language report defined a programming language that was reasonably portable between these systems, though each had their own set of interesting extensions. Our roots as a standardized, multi-implementation language still guide a lot of the structure of the community.
What changed? Part of it is that GHC got a lot better at the aspects that the other implementations had previously had going for them (e.g. GHCi started existing in version 5.00, while folks used to use Hugs for the REPL and GHC for batch mode compilation). Part of it is that other implementations fulfilled their research programs and the authors moved on. Part of it is that the actual Haskell found in the world became more complicated, relying on more language features, and expectations for a language implementation increased over time, making it more and more work to keep up.
The design space of DT is so huge that I believe there’s no non-research language that has proven that it works well across an entire ecosystem.
Which non-research languages have attempted DT and proven that it doesn’t work? The closest I can think of is Idris - where DT has proven to be a massive success.
I do think this is a primary concern with DT - but that is why it’s so critical to comment on ghc proposals that attempt to add new DT-like features to Haskell.
For example: Type Functions is an attempt to introduce staged closed evaluation of terms to Haskell’s type system. The feedback is quite positive - the critics of the proposal have even been swayed! There seems to be no resistance…
People often complain about “DT”, but many don’t seem to complain about specific DT features such as visible dependent quantification and type functions
Idris is a research language in my book.
I’m massively intersested in DT (I find F* extremely exciting and it has actual use cases), but I’m not interested in using DT in Haskell. So I feel there’s nothing to comment. I simply want it opt-in (or not at all).
Since we don’t have competing compilers, we also can’t really have a balanced argument about these things, because GHC is the champion and whatever they decide becomes ad-hoc Haskell.
I know very little about dependent types, but the Motivation section with the sizeOf Bool (vs sizeOf @Bool) example made it very clear why that proposal would make things more ergonomic – I’ll bet I’m not the only one who found @Bool and Proxy confusing and unaesthetic the first time around, or got confused by the error messages around those things. I’ve bumped into them enough without knowing they had anything to do with dependent types. A solution to this sounds like it will be worth a lot.
(I wonder if people have been made more resistant to DT due to these kinds of experiences in Haskell.)
It isn’t just DT:
New type of ($) operator in GHC 8.0 is problematic
…Haskell: now the world’s finest imperative intermediate language?
Some time ago, there was an expression of interest in “embedding Elm in Haskell”. My final remark on that topic was to suggest adding laziness to Elm instead - to me, it seemed a simpler task.
Since the likes of Agda, Idris et al already support [the complexity of] DT, that same suggestion would also seem to apply - it would be easier to implement laziness in Agda or Idris, instead of retrofitting DT into Haskell, as the extra complexity of supporting nonstrict semantics would largely be confined to the implementation.
But perhaps the “dependenting of Haskell” may be a “rip-roaring success” that inspires the embedding of Elm into Haskell: anyone for elm-notation…?
Have you tried a full DT language and observed its errors when you got your code wrong?
Those show case examples of how DT improves ergonomics are 5% of the story maybe. You’ll generally spend a LOT more time staring at the screen when interfacing with DT API that you didn’t write yourself than with current APIs.
And in my opinion, the most interesting use cases, where I would take the cost of complexity, are uninteresting in Haskell anyway (such as cryptography).
DT reducing complexity of the surface language is generally a false statement. It will make it magnitudes more expressive. Expressivity doesn’t come for free. And although it may make some specific use cases easier to express, we won’t be able to remove type families and friends from the language ever. So there’s no cleanup effect for the surface language. Instead you just got more choices and more expressivity.