The future of Dependent Haskell

[atravers]

[…] 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:

• Interpreter and a large collection of library packages

Downloading Hugs

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.

[AntC2]

@int-index

we should not expect that “crawl over cut razor-wire and landmines” attitude of new Haskellers

That’s what we have today. The razor wire beginners have to crawl over is well-documented in the Hasochism paper (2013),

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.

@atravers

[…] 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.

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.

[sgraf]

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).

[AntC2]

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

@sgraf

ScopedTypeVariables are the default (as they should be).

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.

I think you should give Lean a try

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.

[Ei30metry]

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

[atravers]

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

Why can’t I just write:

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

…?

[sgraf]

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

[atravers]

So presumably:

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

would then fail :-b

[sgraf]

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

[atravers]

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

[f-a]

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.

[AntC2]

@int-index

There’s already a plan to merge types and terms, at least syntactically – that’s less code duplication,

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 work on DH is conducted as a series of incremental improvements.

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.

[Bodigrim]

@atravers

Unfortunately the Haskell ecosystem keeps moving on, and like Haskell 98 and 2010, will eventually make the use of GHC 8.10 impractical, even for educational purposes.

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.