# The future of Dependent Haskell

**URL:** <https://discourse.haskell.org/t/the-future-of-dependent-haskell/10614>\
**Category:** Uncategorized\
**Created:** [October 25, 2024, 7:16am UTC](https://discourse.haskell.org/t/the-future-of-dependent-haskell/10614 "2024-10-25T07:16:04Z")\
**Posts on this page:** 1\
**Showing post:** 64

<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 28, 2024, 10:22pm UTC](https://discourse.haskell.org/t/the-future-of-dependent-haskell/10614/64 "2024-10-28T22:22:55Z")

</div>

(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](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html):

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

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

---

_[View the full topic](https://discourse.haskell.org/t/the-future-of-dependent-haskell/10614)._