The future of Dependent Haskell

61

[…] because [DH is] all behind extensions […]

This is of little use to someone whose packages begin to break because their dependencies begin to rely on dependent-type extensions. As I’ve also mentioned before, the Haskell ecosystem keeps moving on, just as it did from Haskell 98 to 2010, and then to now (GHC 2024) - there is only:

www.haskell.org

…there is no:

  • www.haskell98.org

  • www.haskell2010.org

  • www.haskell2020.org

  • www.glasgow-haskell-2021.org

consisting of an “ecosystem-wide snapshot”. So it isn’t possible to “opt out” simply by refusing to use extensions in your own code - you would also have to capture all of the dependencies that your code uses.

In essence, you would be making your own private “mini-fork”…much like what’s provided by the Hugs98+ sources:

Now suppose that the only version of the Hugs98 sources was these:

  • Interpreter and essential library packages […], with other libraries available as separate Cabal packages.

Then Hugs98 really would be dead for all practical purposes, because the Haskell ecosystem (including Cabal) has moved on - most of those “other libraries” would no longer work with a 2006-era Haskell implementation.

1 Like
62

This is an utter misrepresentation: the Hasochism paper is about how hard it is in Haskell as of 2013 to mimic Dependent Typing for advanced Haskellers/typistas. It is not concerned one jot with the experience for beginners to Haskell.

I was about to disagree with atravers that the whole point of putting stuff behind extensions is to insulate the (naive/beginner) user from the dark arts inside packages – especially packages providing low-level interfaces. And several others have made much the same point above. But Π-types break that barrier: if the only way to use a package is calling a function with a Π-type argument, the user is immediately faced with putting types in terms, not merely as narrations. Which leads me to …

The “razor-wire and landmines” is a vivid image but unhelpfully hand-wavy for this discussion. What is it about the beginner’s Haskell experience that’s initially seductive and then rapidly turns sour? For me it was a long time ago, so memory might deceive but …

I’d started programming at school on Dartmouth BASIC. Note types are implicit (as with Logo, another learner’s language). So I got a nasty shock when I encountered ‘bondage and discipline’ languages (Fortran, ALGOL-family, COBOL) that I had to give type declarations for every darned name. Then my joy at meeting Haskell: types implicit in simple cases; how do you know you’ve got beyond a simple case? The compiler starts complaining it can’t figure out the types, so it holds your hand, you can declare enough for a smooth experience. You’re eased into the sensible discipline of giving type decls, at least for your top-level/exportable names.

Hindley-Milner, Hindley-Milner, Hindley-Milner.

Then this is the dislocation beginners encounter: the point they’re forced (rather than merely encouraged) to put type annotations and directives. AmbiguousTypes, ScopedTypeVariables [**], ExplicitForall, … I think this is the point at which my Haskell experience becomes qualitatively different. I ask myself whether I really should be going there.

[**] AFAICT, Lean doesn’t support ScopedTypeVariables (?); it does provide ResultTypeSignatures. Perhaps that tells us GHC has got it wrong. I say GHC there very deliberately: Hugs has always supported ResultTypeSignatures, never ScopedTypeVariables.

Then for me Π-types represent a step backwards to 1970’s bondage-and-discipline typing. I acknowledge there’s a need to use an argument only for its type, not its value, and to be able to declare that to the compiler; and that Proxy or phantom types is a poor fit to that need. I see Π-types as an equally poor fit. (I’ve been reading the Lean manual: if you’re hearing screams from off-stage, that’s me yelling at how stupid it is.)

So my best hope for GHC is that when we do get an implementation of Dependent Typing, people will be able to take a long hard look, and at last understand it was a mistake. Trouble is, by then weyou’ll have another load of legacy code in libraries to maintain forever.

63

I think you should give Lean a try: Functional Programming in Lean - Functional Programming in Lean
I think you might find it not too different from programming in Haskell.
In particular, inference should be roughly on par with Haskell.
Perhaps that might lead you to reconsider some of your opinions about DH (I would hope so), altough perhaps it does not. Still worth the try.
ScopedTypeVariables are the default (as they should be).

3 Likes
64

(I’m trying very hard to avoid this thread relitigating what’s wrong with DH. That ship has sailed.)

ScopedTypeVariables is a specific(ally ugly) GHC extension. Variables (of whatever) are naturally scoped from their point of declaration throughout the smallest enclosing syntactic construct. (I don’t get what you think “as they should be” means.) Take this Lean code:

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | List.nil => Nat.zero
  | List.cons y ys => Nat.succ (length α ys)

-- in Haskell, the signature must be textually distinct from the function def'n.
-- (I'm avoiding DH features for now, but using v8.10 type-mangling):

{-# LANGUAGE  ScopedTypeVariables, ExplicitForAll, TypeApplications  #-}

length :: forall a. List a -> Nat   -- this line could be anywhere in the file
last   :: forall a. List a -> a     -- this `a` is distinct from length's `a`
                                    -- IOW length's `a` has discontinuous scope

length List.Nil         = Nat.Zero
length (List.Cons y ys) = Nat.Succ (length @a ys)    -- this is length's `a`

Lean’s def textually holds together the signature with the function body. But that’s not just a type signature: it also binds the term-level dummy variable xs. It would have been a jolly good idea to support something like this in Haskell before embarking on DH with its tyvars-everywhere bondage-and-discipline. And to more smoothly support that would probably need ResultTypeSignatures – which is a piece of work shunted into the backlog when the decks were cleared for DH.

Did you read my previous remarks? (the “stupid”) Ok, I can start another thread with all I see wrong with Lean, but to give a flavour from that length example:

    def length (α : Type) (xs : List α) ...
    ... => Nat.succ (length α ys)

Whether or not an explicit binding point for the α in the signature would be useful (Haskell has forall), why the f*** would I want to encumber every call to length with a type application when length’s argument ys gives the type? Bondage-and-discipline, unnecessary complexity gone mad. The whole merit of Haskell is (or used to be) you can keep code short and therefore easier to read, and push off the bleedin’ obvious detail to the compiler.

65

You can make α an implicit parameter by wrapping it inside curly-braces instead of parenthesis.

def myLength {α : Type} (xs : List α) :=
  match xs with
    | []      => 0
    | _ :: ys => 1 + myLength ys
4 Likes
66

In that dependently-typed future, a new Haskeller “Leaniant” wonders:

67

You can :slightly_smiling_face: In this case, alpha is implicitly for all quantified.

5 Likes
68

So presumably:

def myLength (xs : List θ) :=
  match xs with
    | []      => 0
    | _ :: ys => 1 + myLength ys

would then fail :-b

69

I should have said any otherwise unbound variable, like theta or alpha, is implicitly universally quantified, just like in mathematics.

5 Likes
70

Programmers Ain’t Mathematicians and Neither Are Testers (original file)

71

The presentation was interesting — although you could summarise your point alongside posting a link, you cannot expect everyone to go through 42 slides to guess what you really meant.

In this case I believe the example you have been shown would fall in the “disguised” category (implicit universal quantification).

Thought-provoking talk nonetheless.

3 Likes
72

Hmm. I worry. Developers have ‘form’ when it comes to re-engineering from the ground up. That bold claim is rather at variance with

The merger will be a rather lumpy increment, methinks.

As a data point (hah!) Hugs internals uses the same structure for types and terms; and although there is a type-specific parser, often in the syntax you don’t know whether you’re starting into a type or a term, so the term parser often gets called to parse types. (After all, they’re both just constructors applied to arguments.) So there’s then some post-parsing rejigging.

OTOH there’s lots of ways term-specific constructor-applied-to-args are different to type-specific constructor-applied-to-args. So that common handling is of limited effect along the compilation pipeline.

73

Fortunately Hackage is a permanent immutable storage and you can easily travel back in time with cabal build --index-state=2010-01-01T00:00:00Z, which uses a snapshot of Hackage at a given date. So even if the ecosystem embraces Dependent Haskell en masse, those who wish to follow old ways (for educational or other purposes) have every opportunity to do so.

6 Likes
74

This is a pernicious, odious, and fundamental misunderstanding about what “totality” actually means. If we are only ever interested in the extensional logical content of code, then sure totality means we’re free to ignore evaluation order. However: (1) That is a conditional argument, not a tautology. (2) The bulk of the consequent follows precisely from the premise that we will never evaluate the code, ergo evaluation order is vacuous. (3) And for some reason I’ve only ever seen folks making this argument in specific circumstances where the premise is known to be false. If someone wants to write programs (i.e., code that gets run), then evaluation order is crucial because it determines whether the code is adequate to perform whatever it is the program should do and the constraints under which it should do them (execution time, resource usage, etc). Unlike proofs, programs fundamentally incorporate evaluation properties that are not captured by the extensional logical content of the code implementing them. (This too is fundamental: if we had a language that incorporated all those evaluation properties, then it would be useless for discussing extensional logical equivalence —precisely because it captures those evaluation details which we would like to be abstracting away.)

Whenever someone brings up the idea of “Lazy Agda”, it is because they are wanting to use “Agda” as a language for writing programs rather than as a language for writing proofs. Retorting that “Agda is total and therefore evaluation order is meaningless” is intentionally misinterpreting what that person is saying.

75

I have no horse in the evaluation strategy race, but as a matter of rhetoric, you’re more likely to persuade hearts and minds, to say nothing of protecting your own social capital, if you stick to the facts rather than imputing bad faith to anyone.

13 Likes
76

Pardon my ignorance, but I don’t understand where you are disagreeing with me. The very first part of my argument (that you chose not to quote) is that you cannot “run” Agda unless you extract Haskell code, which is lazy. Basically lazy Agda.

Only then do I make an argument that unless you want to run a program, evaluation order does not matter (much). This is all to refute the repeated claim that Agda is currently a strict language that somehow needs to have a lazy variant so that proponents of dependent Haskell can just use lazy Agda and let Haskell stay Haskell2010.

6 Likes
77

As for me, there are two reasons why I’ve suggested the addition of laziness to Adga:

  • The length of time needed to transition to a dependent Haskell (but int-index’s task-breakdown page ought to reduce that time drastically, having seen the mass “liking” of posts here which are favour of dependent types :-).

  • The possibility of a future dependent Haskell being total, with the subsequent temptation to then be strict by default:

    and rely entirely on purity to keep effects in check:

    But by themselves, purity and its benefits - referential transparency, ease of parallelism, etc - aren’t having much success elsewhere:

    • The [[pure]] attribute, JTC1.22.32 Programming Language Evolution Working Group (2015)

    • Monad I Love You Now Get Out Of My Type System (14:58)

    • https://web.archive.org/web/20221205155031/https://mail.mozilla.org/pipermail/rust-dev/2013-April/003926.html

      So purity and laziness work better together than apart. Moreover, laziness usually implies purity:

      …which now has to be the only reason why anyone can still proclaim “I/O is pure” in Haskell, or “Haskell is purely functional” - without Haskell’s non-strict semantics, such statements would be that much easier to refute.

So instead of adding dependent types to the last remaining widely-supported non-strict language, make Agda into another non-strict language with similar support - if lazy Agda fails, at least there’ll still be non-dependent Haskell…

78

I’ve started to think of Haskell as a family of languages which each take plus or minus some things from a grab bag of familiar language features, like purity, but crucially a vocabulary (fold, scan, etc) that is reusable in the libraries with a mostly familiar syntax. Glasgow Haskell, Elm, PureScript, Hell, Unison, Roc, Idris. I don’t have to work too hard to think in each of these. That’s a great achievement.

I think it’s not worth competing with GHC as a general purpose Haskell, because it has both the language extensions and the industry grade runtime, with the package ecosystem, so naturally it’s more rewarding to put everything (linear types, dependent type, arrows???, etc) into GHC.

I think it’s possible and practical to do a reset and carve out a niche that Glasgow Haskell doesn’t do well (and maybe doesn’t want to do well), like the other languages I listed. I can give you a clean and simple frontend language (Elm) in exchange for dropping all your beloved language features—many people say, great! (Or give me PureScript.) I could imagine e.g. a simpler Haskell that performs well but compiles lightning fast like Go—that would be worth it for some people in industry where compile times are agony. Maybe Unison or Roc will someday be that.

So for that reason though I don’t personally think much of dependent types (compared to other types of software verification), I kind of accept it as part of the trade off that I also get to greedily pounce on my pet features, that some other people don’t like or care about, every other GHC release, produced and distributed to me as free software.

12 Likes
79

I kind of accept [dependent types] as part of the trade off […]

The people who started these threads were probably also that “accepting” to begin with:

…and as a result both extensions can now only be accessed by using the appropriate command-line options in GHC. But dependent types are different - to many here, "they are the future of Haskell" and (eventually) there won’t be a option to disable them. So if you don’t like dependent types, or just have some doubts about them:

…well that’s just too bad. But there supposedly are plenty of other languages to choose from!
(If you’re content with strict semantics.)

80

Don’t understand this point. [to echo sgraf’s reaction. And Good grief! why didn’t I comment on this claim at the time?]

An important feature of type families/especially associated TFs is that they’re extensible. They fit in with extensible type classes and the module system and separate compilation[**]. Somebody can import my typeclass with its Assoc TF’s; declare their own data types; declare instances of the class and TFs.

Presuming DH’s ‘Dependent Functions’ are like term-level functions, we can’t write open-ended type case. (Also I don’t see what’s hard to grasp about the individual instances of Assoc TFs; they already look a lot like functions.)

What is maybe hard to grasp about Assoc TFs is the ‘distributed logic’ of having instances in many modules/where each data type is declared. But the compiler helps us there: Assoc TF instances can’t overlap/if you want overlap you must use a Closed TF with all its logic in one place.

Now you might say FunDeps are a complex part of Haskell (that is, how they interact across different instances). (Assoc) TFs have already relieved that. So I’m plain not seeing why/how Dependent Haskell will make anything “simpler”.

[**] And follow-up q: I see Agda doesn’t have a thing called ‘type class’, although it does have an overloading mechanism. Does that mechanism count as part of Dependent Typing, or is it an orthogonal feature? How does it fit with modules and separate compilation? Are overlapping instances allowed? If not, how to implement the (fairly frequent) use cases for overlap in Haskell?

In a thread off-forum, we rather came to the conclusion that if you didn’t have type classes, you’d need to invent them (or something practically indistinguishable, including overlaps) to get the power we have in Haskell.