Lean: unnecessary complexity/verbosity [was ref Dependent Haskell]

[AntC2]

@AntC2

I can start another thread with all I see wrong with Lean, …

(continuing the length example from that thread …)

@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

Which shifts the dial from entirely unnecessary verbosity to merely annoying verbosity. @atravers reply reduces the verbosity further, but really the worry with Dependent Haskell is the beginner’s experience/on-ramp for learning about types. Haskell as of early '90’s (and Miranda likewise) you could (and you still can) go

myLength []       = 0
myLength (_: ys)  = 1 + myLength ys

And they can use myLength to get sensible answers. I’m presuming Lean doesn’t allow omitting the sig entirely, so taking us backwards more than 30 years. Did I mention Hindley-Milner?

The compiler infers (some alpha-equiv of) myLength :: Num b => List a -> b.

So the learner asks what’s that Num b => business? Learning opportunity 1: use a annotation to get more precise types:

myLength []       = 0 :: Int

Magic! All the results from myLength are to be Int, due to the power of type unification. Learning opportunity 2 (and a good discipline to get in to):

myLength :: List a -> Int         -- essentially atravers' form

I didn’t need some special announcement to introduce term-level ys in the equation above, I just used it in a pattern; then why should I need some special announcement for a tyvar? Just use it in a type. Why do I have to say a : Type? Just assume kind Type for beginners; by-and-by they’ll find out about other kinds.

So this is a language design principle, which Haskell somewhat observes: default unmarked code to what a beginner probably wants; report type errors where that doesn’t work out; make it easy to add simpler and then incrementally more complex annotations/declarations where somebody (no longer a beginner) wants more exotic stuff.

Do not impose all that bondage-and-discipline on beginners. They already have more than enough to get their heads round.

Now my understanding is that DH won’t mess with that principle: the exotic stuff is explicitly opt-in with named extensions.

But my experience with GHC over the past dozen or so years is that even though I haven’t opted-in, the error reporting/suggestions assume I have.

GHC’s current error reporting that suggests a blanket To defer the ambiguity check to use sites, enable AllowAmbiguousTypes . Naive (and not-so-naive) users tend to grab for this suggestion which a) will only move the ambiguity to the usage site where it is more difficult to diagnose; and b) is liable to allow through other ambiguous signatures that were not intended.

Nobody at GHC HQ gets rewarded for improving the learner’s experience; nor for tidying-up developments that have got beyond the experimental phase, but still are held together with barbed wire (OverlappingInstances/FunctionalDependencies) and gaffer tape (TypeSynonyms), with splinters sticking out (DatatypeContexts).

[AntC2]

(This might be the same point made another way round.)

From these docos about constructing proofs within the type system:

… a function cons which inserts a new element at the head of a list. What type should cons have? Such a function is polymorphic : we expect the cons function for ℕ , bool , or an arbitrary type α to behave the same way. So it makes sense to take the type to be the first argument to cons , …

For “an arbitrary type” – that is, for any type means cons is not just polymorphic but parametric polymorphic in Haskell terms. Then no: it makes no sense for the type to be any argument at all to cons. I want to say not that the term-level arguments to cons “depend on” that type (which is the verbiage used earlier in that section), but rather that the arguments “exhibit” or “instantiate” or “unify to” that type.

It seems that just because sometimes you want to manipulate ‘inside’ the structure of types for Dependent Typing, Lean users are always everywhere paying the overhead of dragging around extra arguments in the surface syntax.

It’s an important feature of Haskell to distinguish ‘parametric’ vs ‘ad-hoc polymorphic’ (aka overloaded). Again it eases learners into the type system that the data structures they first encounter are parametric: Lists, Maybe, Either, …

[eldritch-cookie]

yeah how it is written there is misleading, they also believe its bad as the same section on the new version is completely rewritten