I am giving a keynote talk at the 2025 Haskell Symposium in October. This message is to ask: what, if anything, would you like me to speak about?
One possibility is this:
Towards Dependent Haskell
Over the last few years there have been a lot of improvements in GHC that make Haskell a more uniform, consistent language, including visible type application and abstraction, required type arguments and abstraction, the ability to bind implicit arguments in data type declarations, and so on. These changes all make types and terms behave more alike, a defining characteristic of dependently-typed languages. They have been released incrementally, and their specification is scattered across multiple GHC proposals. In this talk I will bring them together to show how they support some key principles such as lexical scoping. I will also sketch a roadmap for what might happen next.
Another possibility might be to talk about verification of Verse programs.
But I wondered if you had any other ideas? What sort of talks (from anyone, really) would you like to hear?
Time is short: I have to decide on something by Friday!
Itâs would be exciting to hear about a potential future Dependent Haskell, but I am also curious about the past. I know about the paper A History of Haskell:
Being Lazy With Class from 2007, but it seems like some parts are not reflective of the current culture. Or maybe they are? It would be interesting to hear which are/arenât considered current.
For example
An entirely unforeseen developmentâperhaps encouraged by type classesâis that Haskell has become a kind of laboratory in which numerous type-system extensions have been designed
Do you still see this as Haskell/GHCâs role? I am not a compiler developer but, it seems to me that GHCâs implementation might be considered too large for some experiments (which?). This might just be me parroting unwarranted hearsay and conjecture.
The section about Haskell 98 also feels like it might not be accurate enough any more:
In contrast, the Haskell community is small enough, and agile enough, that it usually not only absorbs language changes but positively welcomes them: itâs like throwing
red meat to hyenas.
How is this paragraph to be interpreted in the context of the Extensions Categorization? Does it mean that CUSKs or any of the other legacy extensions could be entirely removed from the compiler?
If these questions canât be answered very easily, then that would also constitute an answer to me.
Iâm more interested to hear about âsoftâ topics: how to develop a language in a large open source community?
Haskell started as a specification to unify scattered efforts of lazy functional languages. At some point GHC got the monopoly. We donât work on the report anymore, but have a GHC SC committee. There are interactions with other committees. There are diverging ideas about what Haskell should be, how the compiler should be developed.
Different generations had different priorities. âStabilityâ has seen a rise in recent years.
What does the godfather of Haskell think about the evolution of Haskell? What can we learn from it?
A successful keynote frames the entire conference by setting the overall theme and direction, fostering active discussions and debate, inspiring attendees to take action, and integrating new ideas into the discourse. That holds even for highly technical meetings such as the HS. Obviously you can give a highly technical DH lecture anywhere, anytime. But a keynote is different, thatâs a distinct, foundational talk for a conference.
In that light, @hasufell is spot on: Discussing a bigger picture is the way to go. A few possibilities to stir discussion (making this post into a meta-keynote
Where have we been, where are we going? How have we influenced others?
How do we trade-off being a successful research platform and a successful production platform, when those have competing needs? For example, backwards compatibility, technical debt, language and API deprecation, ease of onboarding practitioners, quality of tooling, and so on.
Where do we want to be on the PL complexity-simplicity spectrum?
Of course youâre speaking as yourself, so itâs great to propose answers to these big questions. If thereâs subsequent discussion and debate, and if thereâs community engagement, then the keynote is a great success.
Simon, if youâre going to talk about Dependent Haskell, Iâd like to know whether it could ever achieve the kind of full safety we see in Agda or Lean4. From what Iâve read, including the current effort (Seroquel) and most research papers on Dependent Haskell, the design is always about enabling dependent types for proving useful properties of programs without totality checking and without full immunity from logical paradoxes (like Girardâs paradox).
The absence of totality checking is expected to impact Dependent Haskell programs, because proofs would need to be run at runtime. The lack of full immunity to Girardâs paradox is usually considered a problem only in extreme edge cases.
I believe totality checking might be encoded within Dependent Haskell itself (part of it would resemble proving substructural recursion). But proving that programs donât suffer from Girardâs paradoxâI have no idea whether that could be done without re-engineering GHC again, the way introducing Dependent Haskell already required.
Should users be able to prove totality encoded inside Haskell itself, without extending the language. Runnable proofs could in principle be optimized away by the users, because GHC supports rewrite rules. If a proof were declared total, rewrite rules could be used to erase said proof from runtime. (Iâm not entirely sure I explained this last point correctly, but thatâs the idea.)
For comparison: Idris2 is my main and favorite programming language. It has always supported totality checking, but Girardâs paradox is not dealt with (again, this only comes up in extreme cases). Itâs expected that Idris2 ( or idris 3 ) will eventually handle it, since the surface language wouldnât need much change to incorporate the techniques Idris1 already experimented with.
Another point: will Dependent Haskell imitate Idris2 in how it separates proofs from runtime data? In Idris2, data can be:
normal (used freely at runtime),
1 (linear, must be used exactly once at runtime), or
0 (erased, never used at runtime).
This separation is really powerful, and in general I think Dependent Haskell should ârip offâ Idris as much as possible.
Indeed. Simon co-authored a proposal that would in effect bless row types.
As the paper notes, SML-alikes already supported a form of row types. Idris has them; most haskellish languages since have preferred stand-alone records rather than the named fields for ADTs.
iâd be interested to hear if Dependent Haskell might one day get us to extensible/stand-alone rows/records. ( The Trex prototype kept within Hindley-Milner + typeclasses. )
Dependent Haskell sounds interesting. In the direction of getting a broader picture, here are some questions that a presentation could visit. Much of these questions overlap with each other.
Why should Haskell become dependently typed? Is it going to make programs simpler? Is it going to be better than using ChooseYourFavoriteDependentlyTypedLanguage for some problem? Is it going to enable further experimentation?
With so many proposals, Dependent Haskell sounds like a titanic effort, while other languages designed with dependent types from the start seem to move faster. What are the main advantages of arriving to dependent types in the Haskell way?
How could we expect Dependent Haskell to be different from other dependently typed programming languages?
I am working on documenting and writing tooling for Cmm. The GHC code generation IR
( i post updates on discourse with this user )
My mentor for the aforementioned GSoC project is working on alternate backend for GHC :
STG â His own backend â Cmm. Cmm is used so it can initially reuse the GHC rts, however
he plans to eventually replace the traditional rts with one produced with automatic code synthesis.
Sorry if this isnt what you were looking for . I gather not many people have worked on alternate GHC garbage collectors because replacing the rts is a tall order. At least there is still microhs with its own runtime
Could you elaborate what you mean by open problems?
Thank you for all the suggestions! In the end, after consultation with the committee, Iâm going to do a talk on join points.
Join points in practice
Abstract: Eight years ago âCompiling without continuationsâ introduced the idea of so-called join points as a powerful optimisation tool in a functional language compiler. Since then join points have become more and more deeply entwined in GHCâs optimisation passes; for example they are treated specially by the Simplifier and its Occurrence Analyser, and a dedicated pass called Exitification makes a join-point-specific transformation
With the perspective of this experience, I am convinced that any serious functional compiler should use join points (or something equivalent): itâs a powerful and re-usable idea. Yet beyond the initial paper, none of what we have learned has appeared in print. In this talk I will share the lessons of the last eight years of using join points in practice in GHC.
I remember watching the talk about Compiling without continuations long ago, which a quick youtube search reveals has apparently been reuploaded by the haskell foundation. Interested to see how things have changed since then.
Very interesting. Given that racket ( a scheme ) is my second language ( after idris2 ) . I tacitly considered continuations to be an end all, be all of functional programming
For a historical comparison, âJackson Structured Programmingâ [1975 COBOL, see wikip] included something called Common Action Tail [which Google seems not to know of]. This was implemented via the dreaded GOTO a label near the end of the subroutine. [wikip on GOTO/Tail Call quotes Guy L Steele 1977] CAT is more generally applicable than Tail Calls. (And COBOL of that era didnât support recursion.)
Dependent Haskell sounds interesting. In the direction of getting a broader picture, here are some questions that a presentation could visit. Much of these questions overlap with each other.