From my limited experience with F* and liquidhaskell, I wholeheartedly disagree. It’s a great tool to have these things, but it also adds a constant layer of additional reasoning to your everyday programming. Especially if it’s more powerful and natural to use.
No. On a technical level. Exposure to APIs will do that.
From my limited experience with F* and liquidhaskell, I wholeheartedly disagree. It’s a great tool to have these things, but it also adds a constant layer of additional reasoning to your everyday programming. Especially if it’s more powerful and natural to use.
To be clear, I was referring to the hodge-podge of features within GHC, not liquidhaskell. Dependent Haskell doesn’t subsume liquidhaskell any more than GHC Core subsumes type classes.
No. On a technical level. Exposure to APIs will do that.
For point, the fact that GHC doesn’t attempt to audit whether imported interface relies on disabled extensions is a travesty that should be fixed.
I am hoping Remove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc (#18758) · Issues · Glasgow Haskell Compiler / GHC · GitLab will enable that. So long as just remember module interfaces with core types, we are mostly prevented from understanding the language features involved. Once we properly distinguish surface language vs core types, we can also store the former in hi files. This will greatly improve this and many other manners of ergonomics.
We are indeed coming up on 10 years of fears about DH.
The Committee has decided to proceed with DH. Can I suggest we all just shut up and stop distracting those who understand DH and are competent to implement it.
I don’t understand. (I’d describe myself as hostile to DH – or at least hostile to all the proposed syntax that’s growing like a carbunkle on the face of a dear friend).
Clearly I’m too stupid to understand. Probably I’m too stupid to ever write DH. (Although I’m happily using FunDeps to achieve what seems to be the same outcomes – and yes we’re coming up 20 years on using those techniques.) Perhaps I might benefit from packages written using DH. But I’m never going to find out unless it actually gets delivered.
So just stop the hubbub.
Are we really sure “the current hodge-podge of features” is going more-or-less in the direction of dependent and not dynamic types?
If some new language were to appear that had:
…could it be seen by some as a potential [dependent] Haskell replacement?
Edit: @AntC2’s message has already clarified that DH is the future of Haskell, so I’ll stop with my hubbub on this topic as suggested: look before posting in case someone else was “faster on the keyboard”…
Good question. When I see examples of DH that seem to make types depend on values that can’t be known until run-time, that reeks to me (in my not-understanding) of dynamic types. Divide by zero, numeric fixed-width overflow, subscript out of array (when the subscript arrives at run-time). It’s just perversion to re-label those as type errors: type-assignments/type inference/type-safety are what you get statically at compile time. If a program crashes at run-time because of divide-by-zero, don’t tell me that’s a type error, because type errors don’t happen at run-time.
But again, we’re not going to find out unless we let the people get on and deliver it.
Uhm I don’t think typical dependently typed programs would call divide-by-zero exception type error. Coq does not allow such division to happen, and I believe it is the same for Agda/Idris too. Yet they still have the concept of “values not known until runtime” - which is the core feature of DT (depending on unknown values as variables).
It’s just that some computation will happen in compile-time, and give errors if desired constraint is found hard to meet. This kind of errors never happen after compilation into machine code / anything else.
There are things that one can write with dependent types that I would consider poor taste, but rest assured they are not dynamic types.
Types that are not known until runtime are “skolems” at compile time. And they are still erased so there is no “actual” substitution of those parameters for concrete types at runtime.
I feel bad seeing this out in the open, but to really understand the idea that (erased) types depending on values is only “demonstrated” by specializing values at compile time, is also to see that perhaps dependent types are not the perfect calculus. E.g. Quantitative Type Theory rubs me the wrong way (It is just saying we can always lossily remove the linear bits, like projecting a shadow to a lower dimension, in order to get the “type level” version of the run time thing, but that strikes me as too simple/strong.)
All this to say is a IQ Bell Curve / Midwit | Know Your Meme sort of thing: there are I believe valid advanced ways to critique dependent types, but one has to pass for through the “hell yes I love them” stage first to reach those critiques, and even then I am not sure whether they are true, just merely plausable enough to warrant consideration. (I would certainly not consider myself expert enough to make any sort of call on that!)
And, bottom line. Even if one of those critiques turned out completely true, and Dependent Haskell is not the end state, it’s not a dead end either — I would still even with clairvoyant knowledge of that say we should do DH, again for the main purpose of cleaning up our current hodge-podge.
This is a fascinating thread. I want to add that I’m in a similar camp as @simonpj on this, as expressed in his post.
I strongly believe that the future leads through dependent types. Indeed, I’ve come to view non-dependent types as quite a strange way to set up a programming language. If a language should have types at all, it should have dependent ones: otherwise, some of the ideas you wish to express are inexpressible. But – in some contrast to the me of 5 years ago – I’ve come to be more skeptical of adding dependent types to Haskell as it exists today.
Suppose we’re renovating our castle. We know that a beautiful tower placed just there will be a sight to behold – and will give us a wonderful view, both for pleasure and for sound defensive strategy. I was part of the team that planned out the tower and worked on convincing many of where it should be placed and why it would be so nice to have. Yet, as I’ve been actually constructing the tower, I’ve noticed that the part of the castle under which the tower will go is not quite so soundly built. There are parts of the castle that are already crumbling, and others which are fine today, but probably won’t support the weight of the tower. This all means that we probably shouldn’t proceed, today, with tower-building. Instead, we should work on building up the structure underneath the tower so that it will support that tower well and for a long time.
Returning back to dependent types: the support for dependent types is not strong enough yet in Haskell to support it. There are at least two dimensions to this:
HsExpansion plan, adding support for proper predicates, making type families compute faster, adding support for HsType GhcTc, and probably more I’m overlooking).Perhaps once these foundational issues are sorted out, we’ll be in a better position to build actual dependent types.
This does not mean work should stop! Indeed, the current proposals process – for all its apparent slowness – is doing an excellent job of figuring out where the current edifice is strong enough to support continued building. And so we continue to build in the direction of dependent types. At the same time, I’ve pivoted somewhat to focus more on user experience, knowing that others (hat tip to @int-index and his collaborators who, among others, are pushing this forward) are doing the work on dependent types directly.
So work continues apace. Some of it is invisible (refactorings within GHC), just like one might expect in a renovation of a structure where new weight will be added on top. Some of it is user-facing (I think the improvements in HLS are essential in order to support dependent types properly). But I do think we will – almost inevitably – get there in the end.
Yup. That’s exactly it.
Perhaps different people want different incompatible towers. But surely we can all agree to repair the castle. Let’s do it!
Who would be best to share with us a more detailed review of the shoring up that needs to be done in GHC? Even better, is this at the level of effort where we need to have an actual engineering plan with coordination and possibly even sponsored work to get us through that plan?
Are you asking @rae, me, or both? Regardless, yes I would like that.
I have felt sort of stymied that HFTTs proposals are both a) discrete proposals, and c) must have some sort of HF funding component. I would like to have some sort of big living roadmap where we lay all these behind-the-scenes bits out (in various levels of detail). It’s less itemizing the individual parts of the “castle” that needs repairs that interests me, than the big weaving them together into a single holistic plan, that I think is the more important.
First figure out what we want, then figure out when we want it (who wants to pay for what parts and how to much to make it happen sooner).
Well, for practicalism, some would suggest not changing it at all. Stability and status quo could be great for continued usage.
Status quo is not sustainable. The other languages will absorb Haskell features over time and there would be no more “future GHC maintainers”.
I’d rather help people with “continued usage” while the core gets rebuilt than have it stagnated.
Uhm, which languages would absorb haskell features, you mean?
I view that as a strange opinion about programming languages: current mainstream languages are somewhere in a continuum: untyped - weakly-typed - statically-typed - dynamically-typed. So Dependently Typed languages are currently a niche. (Unless you want to clump dynamically-typed as a variety of dependently-typed – but the threads for Haskell are saying the DTs are not related like that.) How did strongly-typed languages manage to survive 60 years and still be mainstrean? (starting counting from Algol 60).
“inexpressible” is just plain wrong: those languages keep sophisticated software systems going. It might be some ideas can be expressed only poorly/requiring extra code in which the compiler can’t see the invariants the code is successfully expressing.
But then even with Dependent Typing, there remain ideas you can express only awkwardly. (Catching overflow or divide-by-zero of values that arrive at run-time.) So there’s a value judgment: does the increase in expressivity outweigh the disruption of introducing Dependent Typing, and the cognitive load all users will need to carry?
This tower? [†] Or the highest human construction in the world – at the time of its second collapse. (Before anybody asks, the Burj Khalifa is the opposite of beautiful – and that’s before you find out about what happens with its sewage.)
I agree the current under-structure needs some remedial work. I disagree what that work should be addressing – so if I were to continue with GHC I’d be suffering all the disruption and cognitive load with no improvement in what I want to express.
[†] Addit: (for those not getting the relevance to language, and amidst the loose talk of forking tongues) "That is why its name was called Babel—because there the Lord confused the language of the entire world, " — Genesis 11:9 NET
Thorough dependently typed languages do not allow such overflow and divide-by-zero to occur - because that harms soundness. Not that those dependent typed languages are practical tho, like, they’ve been around for long and is still strictly constrained to niche uses.
I wonder if replacing types entirely with tests would work for future languages. In the end, tests are sufficiently powerful and flexible.
Rust, Scala, Java. You know, the languages.
I don’t see Java absorbing Haskell’s features, it is only recently adding some of pattern matching.
In my eyes, Scala is too big to absorb extra features. Also I’ve seen many backlashes against haskell style there.
I guess Rust is a valid contender, but thankfully they are usually for distinct lower-level niches. Would its borrow checker be happy with the abstractions haskell provides?