I honestly do not understand the type spaghetti argument.
Dependent Haskell would likely reduce existing type spaghetti in libraries, by e.g. allowing partial application of functions at the type-level. I don’t see how making types easier to manipulate will mean that abstractions that are possible now will instead be implemented in an overly complex manner.
However, I do think that we will see complex abstractions that simply weren’t possible before.
2 Likes
(code/type) spaghetti isn’t a result of lack of expressivity. It’s the opposite.
This is as much a social experiment as it’s a technical one, but I hear only discussions about the latter.
Quoting from https://artandlogic.com/2021/08/exploring-dependent-types-in-idris
As the code that you’re formally verifying becomes more complex, implementation quickly goes from easy, to time-consuming, to an active research area.
We’re creating a new language, incrementally, that will not be anything like what Haskell was, if it succeeds. Maybe that’s good, maybe it’s not. That will depend on the users of the language. Who will buy into it? How will they use it?
This has never been done before in a mainstream language, has it? Yes, I consider Haskell mainstream.
Many Haskellers can barely keep up with all the tools that we already have, see Stephen Diehl’s great compilation.
Dependent types being entirely opt-in would solve this issue. But again: a language pragma is not opt-in. I’m not saying I know what’s best, I’m just raising these concerns.
1 Like
@hasufell your arguments make sense to me in the abstract, but do not fit the facts as I see them.
We’re creating a new language, incrementally, that will not be anything like what Haskell was, if it succeeds. Maybe that’s good, maybe it’s not. That will depend on the users of the language. Who will buy into it? How will they use it?
No, that is what we’ve been doing the past 10-20 years. The current hodge-podge of features vaguely gesticulating in a Dependent Haskell direction. The direction of gesticulating is not the problem. The hodge-podge doing the vague gesticulating is.
This has never been done before in a mainstream language, has it? Yes, I consider Haskell mainstream.
C++11 made a lot of new stuff. The ickiness vs something like Rust was that there was no stomach for getting rid of bad old stuff. We thankfully don’t need to get rid of anything! Certainly not in Haskell 2010. I would advocate getting rid of type families, but this is purely optional; we can support them along-side the better alternative indefinitely.
Many Haskellers can barely keep up with all the tools that we already have, see Stephen Diehl’s great compilation.
That’s because we have the hodge-podge. Once we unify the current mess into Dependent Haskell, it will make more sense not less!
Dependent types being entirely opt-in would solve this issue. But again: a language pragma is not opt-in. I’m not saying I know what’s best, I’m just raising these concerns.
On a technical level it sure is opt-in. You mean on a social level? Sure, but we already have that problem today with the hodge-podge. If we have that problem regardless, I don’t see this as an argument not clean things up.
2 Likes
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.
1 Like
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:
- Erlang’s features; at least the one which could be supported alongside non-strict semantics (including being dynamically typed)
- Haskell’s syntax; again those which had a one-to-one correspondence with Erlang syntactic features;
- a source-language “verifier”, analogous to what Sun devised for Java bytecode, to detect obvious errors like finding the square root of a string;
…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.
1 Like
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.
2 Likes
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:
- The code within GHC still needs to be cleaned out in order to become more extensible. This is underway in a variety of directions (e.g. for the cognoscenti: the new
HsExpansionplan, adding support for proper predicates, making type families compute faster, adding support forHsType GhcTc, and probably more I’m overlooking). - The user-facing interface to the language needs to be more accessible. While I can claim (and do!) that adding dependent types need not worsen any existing error messages, I’ve come to agree that adding the feature will make the language harder to learn – at least in the first iteration of dependent types. Dependent types are new and strange to many. (I claim they can be seen as simpler than non-dependent types, but that won’t help the legions of people coming to Haskell from other typed languages.) Haskell is already unnecessarily hard to get into. It comes with too many unfamiliar concepts, and there is not a good way to discover how these concepts fit together. Fixing this well will require educational resources, improved IDEs, and better error messages.
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.
17 Likes
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!
7 Likes
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?
1 Like
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).
1 Like
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.