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

**URL:** <https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633>\
**Category:** Uncategorized\
**Created:** [October 29, 2024, 2:06am UTC](https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633 "2024-10-29T02:06:38Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 29, 2024, 2:06am UTC](https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633/1 "2024-10-29T02:06:38Z")

</div>

> [@The future of Dependent Haskell](https://discourse.haskell.org/t/the-future-of-dependent-haskell/10614/64):
>
> I can start another thread with all I see wrong with Lean, …

(continuing the `length` example from that thread …)

> [@The future of Dependent Haskell](https://discourse.haskell.org/t/the-future-of-dependent-haskell/10614/65):
>
> You can make α an implicit parameter by wrapping it inside curly-braces instead of parenthesis.
> 
> ```haskell
> 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

```haskell
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:

```haskell
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):

```haskell
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](https://github.com/ghc-proposals/ghc-proposals/blob/c9401f037cb22d1661931b2ec621925101052997/proposals/0232-AmbiguousType-pragma.rst#L7).

> 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`](https://mail.haskell.org/pipermail/hugs-users/2022-July/000935.html)).

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 29, 2024, 5:27am UTC](https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633/2 "2024-10-29T05:27:05Z")

</div>

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

From [these docos](https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types) 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, …

---

<div class="post-metadata">

**Author:** ![eldritch-cookie](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/eldritch-cookie/32/4130_2.png) [@eldritch-cookie](https://discourse.haskell.org/u/eldritch-cookie)\
**Post date:** [October 29, 2024, 3:30pm UTC](https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633/3 "2024-10-29T15:30:27Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 29, 2024, 10:00pm UTC](https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633/4 "2024-10-29T22:00:59Z")

</div>

Hmm? Thanks for pointing out there’s a Lean4 version. Seems to be exactly the same wording “[So it makes sense to take the type to be the first argument to `cons` , …](https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#what-makes-dependent-type-theory-dependent)”. There is a revised `def` for `cons`, with a superfluous IMO first argument giving the element type.

The later text also seems to be much the same as Lean3:

> This is a central feature of dependent type theory: terms carry a lot of information, and often some of that information can be inferred from the context. In Lean, one uses an underscore, `_` , to specify that the system should fill in the information automatically. This is known as an “implicit argument.”

> It is still tedious, however, to type all these underscores. When a function takes an argument that can generally be inferred from context, Lean allows you to specify that this argument should, by default, be left implicit. This is done by putting the arguments in curly braces, as follows:

So I guess we end up just about the same place as Haskell today, with explicit `forall`s and type `@`pplication. I’m not seeing leaner nor cleaner.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [October 31, 2024, 8:34am UTC](https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633/5 "2024-10-31T08:34:08Z")

</div>

I’m struggling to find in the Lean docos a clear example of a function returning a `Type` (as opposed to returning a value of some dependent type). Down in the weeds of an [exercise for type-safe access to a database](https://lean-lang.org/functional_programming_in_lean/dependent-types/typed-queries.html#nullable-types) there’s:

```haskell
structure NDBType where
  underlying : DBType
  nullable : Bool

abbrev NDBType.asType (t : NDBType) : Type :=
  if t.nullable then
    Option t.underlying.asType
  else
    t.underlying.asType

```

So the `: Type` for `asType` means it returns a type. But that’s an `abbrev`, not a first class function:

> [Definitions written using `abbrev` are always unfolded](https://lean-lang.org/functional_programming_in_lean/getting-to-know/functions-and-definitions.html#messages-you-may-meet).

This sounds more like a Haskell `type` synonym, although `asType` has some conditional logic/the scrutinee is a type not a term. Note `underlying : DBType`, so this is a different namespace (introduced earlier in the exercise [\*\*]); `t.underlying.asType` is therefore ref’ing a different `asType` defined in that namespace `: DBType -> Type`. Then:

- In `t.underlying`, the `.` is field access;
- in `t.underlying.asType`, the second `.` is applying function `asType`, to return a `Type`.

Then here’s an example usage from earlier, declared using an ordinary `def` but then it’s returning `Bool` not `Type`:

```haskell
def DBType.beq (t : DBType) (x y : t.asType) : Bool := 
  match t with
  | .int => x == y
  | .string => x == y
  | .bool => x == y

```

Boolean equality for fields of types available in the database. The scrutinee of the `match` is `t`; then the `=>` must refine the types for `x, y` so yielding typesafe despatch to the appropriate overloading for `(==)`. Since the RHSs of those three `=>` are identical and `(==)` is already overloaded, it’s not abundantly clear to me why the compiler needs so much ~~bondage-and-discipline~~ hand-holding.

[\*\*] Or a different data structure? declared using keyword `inductive`, not `structure`. And I’m not getting why using the constructors from that `inductive` needs a dot prefix (`.int`); there’s no dot in the decl.

---

<div class="post-metadata">

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\
**Post date:** [October 31, 2024, 10:27am UTC](https://discourse.haskell.org/t/lean-unnecessary-complexity-verbosity-was-ref-dependent-haskell/10633/6 "2024-10-31T10:27:15Z")

</div>

`abbrev` is like `def`, but always unfolded during type-checking. You may still bind higher order functions this way and apply them as well.

The more general pattern where we define a function mapping an ADT into Type is called the universe design pattern: [The Universe Design Pattern - Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/dependent-types/universe-pattern.html)

Edit: note that use of == would require (the equivalent of) an Eq instance. Unless asType is abbrev, you could not solve this instance in each match branch. There is no EQ instance for `DbType.int.asType`; only for `Nat` (or whatever).