The future of Dependent Haskell

#54

Any definition of what it is for DH to be ‘finished’.

Π-types and function promotion. We get that and we’re in dependent types land.

Any timescale for delivery.

No timescale and no promises. We’re doing it as a series of incremental improvements, so if development stops one day, it’s still a net positive for the language.

Any enumeration of non-DH features/fixes or extensions that would be paused or for how long.

None. Zero. I don’t get where you get this idea that DH interferes with development of other features. This is not a resource allocation problem where I either work on DH or some other Haskell feature. I’m interested in DH specifically, so it’s either that or nothing at all.

So in effect there was a whole backlog of accepted enhancement requests that were just nuked.

That never happened. If there’s some accepted GHC proposal that you’d like implemented, the way forward is to step up and submit a patch.

The GHC Steering Committee does not hand out tasks to contributors, it simply approves or rejects language changes that volunteers want to implement. No volunteers – no implementation.

how much more complex GHC’s internals would get, such that any later attempts to revive those features would turn out to be greater effort than if GHC had never done DH

What makes you believe the internals are getting more complex? They’re getting simpler. There’s already a plan to merge types and terms, at least syntactically – that’s less code duplication, more uniformity.

and which I suspect will be more difficult to engineer in DH-riddled GHC

The work I do on DH goes through many rounds of code review. We’re not getting a “DH-riddled GHC”, the engineering quality is as high as ever. Rather, we’re getting “DH-enhanced GHC”, and it doesn’t preclude the work on any other feature, even when it comes to very ambitious features like LinearTypes.

if you’re sure you don’t want a language with Dependent Typing, now is the time to get off the bus

The opt-in principle is enshrined in #378, and we follow it. I challenge you to show a program that you can no longer write due to the work on DH done so far, or that you imagine will be invalidated by future work.

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), and it took me a detour to Agda before I figured out how to use GADTs and TypeFamilies effectively. The entire idea of DH is to sidestep all of that with a proper implementation of dependent types.

I repeat: the work on DH is conducted as a series of incremental improvements. Worst case scenario is that the language is improved moderately instead of improved greatly.

specifically the error messaging suggesting AllowScopedTypeVariables

There’s no such extension. You either mean AllowAmbiguousTypes or ScopedTypeVariables, and neither extension is part of DH. You can nuke both of them from orbit, or at least remove them from error message suggestions, and it won’t affect DH in the slightest.

Any other concerns I could address?

31 Likes
#55

The razor wire beginners have to crawl over is well-documented in the Hasochism paper (2013) […]

(While mentioned thrice in #378, this is the first time it’s been referenced here on this Discourse.)

#56

The razor wire beginners have to crawl over is well-documented in the Hasochism paper […]

By the time a Haskell has their first encounter with dependent types, they should no longer be a beginner. But as has happened with some other type-level entities, there is the risk of new (“What’s Haskell?” ) Haskellers having that encounter at the very beginning, while they’re being introduced to other concepts such as:

  • call-by-need instead of call-by-value
  • binding instead of destructive assignment
  • functions free of side-effects, instead of imperative procedures
  • static types instead of dynamic types

and so forth. Hence my concern expressed here:

#57

If they perceive “the learning curve” of a “Dependent Haskell” to be too steep, they will simply go elsewhere…

I don’t see how this is different from the current situation where beginners might be exposed to DataKinds, PolyKinds, GADTs, TypeFamilies, RankNTypes, etc.

In fact, you write:

as has happened with some other type-level entities

So is there a reason you want to single out dependent types? In a beginner’s mind, wouldn’t it all register as “advanced type-level Haskell” without fine-grained distinctions that would make DTs more intimidating than, say, type families or kind polymorphism?

7 Likes
#58

In a beginner’s mind, wouldn’t it all register as “advanced type-level Haskell” […] ?

Only if the beginner doesn’t have an adverse encounter with dependent types while trying to understand the basics of declarative functional programming (in Haskell). Otherwise there’s the risk of Haskell being perceived as the programming-language equivalent of an IQ test.

So is there a reason you want to single out dependent types?

For the same reason as I’ve also been doubtful of functional dependencies, and every type extension which has attempted (and failed) to replace them - the ability to program at the type level (which, in the case of functional dependencies, I have previously referred to as poor-man’s Prolog).

…or for us:

  • Less code means less bugs.

So expecting future Haskellers to write more code in the form of proofs, propositions, and other artifacts of logic can only result in more bugs. Given the first-class status of both values and types in a future dependently-typed Haskell, just how smart will people need to be to debug that code?

#59

Thanks @int-index for your long post, but I really really don’t want you to use up your time with the grumblers on Discourse (including me).

I disagree with nearly everything you claim. It’s pointless continuing; we’re merely repeating entrenched positions. Suffice to say, I am so disappointed with the direction of GHC, I’ve given up. It’s not just one or two topics (so not DH specifically, although I now realise there’s much that was groundwork for it); it’s pretty much everything GHC has addressed – and more importantly failed to address – since around 2016. I find Hugs (as modified by me) superior for my Haskelling purposes in every way to GHC 8.10 other than not providing PatternSynonyms – even for that I’m lukewarm.

I feel I’ve volunteered heaps. It’s been thrown back in my face. So I’ve implemented in Hugs.

To provide some balance here, I did say as my first response above:

That is: for those who are continuing to keep up to date with GHC, DH is not making the experience significantly worse, because it’s all behind extensions (as several have pointed out).

#60

I think that reading code with DH is more counter-intuitive, but I totally agree with @int-index that:

  1. DH makes inner magic just visible and accessible to everyone
  2. DH with merging types with term makes code more uniform and this allows to get rid of code duplication

Hopefully DH does not block alternative language developing!

1 Like
#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.

Lean: unnecessary complexity/verbosity [was ref Dependent Haskell]
#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
3 Likes
Lean: unnecessary complexity/verbosity [was ref Dependent Haskell]
#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.

4 Likes