The future of Dependent Haskell

[atravers]

In a thread off-forum, we rather came to the conclusion that if you didn’t have type classes, you’d need to invent them […]

(…“rather” would be an understatement).

[sgraf]

My point was: If you want a closed type family, you actually want a type-level function. If you want an open type family, (I will question your design, and) you can often replace it with an associated type/type method of a type class. Note that although GHC chooses to compile associated types similarly to open type families, that need not be the case. For example, in a dependently-typed language, an associated type of a type class is simply a type-valued method, as I exemplify below using Haskell syntax:

type family F a b :: Type
type instance F Int Char = Bool
...

==>

class C a b where
  f :: Type
instance C Int Char where
  f = Bool
...

(Yes, would need -XAmbiguousTypes. Can be worked around with some of the visible forall improvements that are ongoing, I think.)

Now the evidence for a C Int Char constraint contains means to concoct a proof for f @Int @Char ~ Bool, similar to F Int Char ~ Bool in the original program (although I’m not sure if Dependent Haskell would in practice choose to represent definitional equality as coercion axioms.)

Agda does not have a separate syntax for type classes; you simply declare a record type and register implementations for instance resolution using the instance keyword, then request them using {{eq : Eq Int}} in your function type.
Lean uses a similar mechanism but offers the syntactic sugar of class and instance declarations (i.e., declaring a record, its implementations and registering instances for tabled resolution)

[AntC2]

@sgraf

If you want a closed type family, you actually want a type-level function.

I’ve always taken it from the get go (2008) that Type Families are functions at the type level. The implementers chose not to call them “functions” (but did choose a name starting f ) because:

• Many of the constructs you can use in term-level expressions make no sense in types.
• TFs must be ‘evaluated’/reduced at compile time, so that type inference/checking/instance selection can complete.

@sgraf

GHC chooses to compile associated types similarly to open type families, that need not be the case.

I’m pretty sure you’re wrong there: all the docos say an Assoc type decl is simply alternative syntax for a Type Family. “A data or type synonym family can be declared as part of a type class” [quoting from the section linked below]. If you think they’re two different things, then you’ve over-complicated it, and your “simpler” claim above is merely because you haven’t realised Assoc types simply are TFs.

@sgraf

If you want an open type family, (I will question your design,

Again I disagree: open TFs/equivalently Assoc types are the replacement for FunDeps. They must be open because class/instances are open, so FunDeps are open. Again you’re describing the existing situation as more complex than it is, and Dependent Typing is no simpler.

You perhaps think TFs can’t be like functions because they’re spelled upper-case. That was a stupid design choice: everything else spelled upper-case in Haskell is injective. If I had a penny for every time I thought I was looking at a type only to realise it’s a TF call …

@sgraf

simply a type-valued method

There’s nothing “simply” about a method that has to return a type not a value and be able to do that statically at compile time. Its arguments also have to be (interpreted as) types, for example.

@sgraf

would need -XAmbiguousTypes …

That example is crying out for a FunDep. Think of a FunDep as simply a type-valued method; but placed syntactically in the class/instance header so you can see what its arguments are. Also why isn’t f declared like a sensible method?

class C a b where
  someMeth :: a -> b -> f a b    -- f has arguments, doesn't it?
  f        :: a -> b -> Type     -- so it needs a signature to show that  [**]

instance C Int Char where
  someMeth x y = last (show x) == y
  f        _ _ = Bool            -- [**]

[**] Oh, but the arguments to f-qua-method in its signature can’t be named as a b because in a method signature that denotes the type of a term. Never the less, the binding for f within the instance might want to call and pass arguments to some other type-valued function, so it does need a mechanism to name its arguments. Consider for example instance C Int (b1, b2) where ... in which f needs to examine b1 . Or indeed the more complex examples in the docos

6.4.9.4. Associated data and type families
The type parameters must all be type variables, of course, and some (but not necessarily all) of then can be the class parameters. Each class parameter may only be used at most once per associated type, but some may be omitted and they may be in an order other than in the class head.

And why are you calling f using that @ syntax? If you’re telling me it’s simply a type-valued function, why aren’t its arguments simply type-valued expressions (aka Types). And why are you talking about “concoct a proof”? I don’t say “concoct a proof for 1 + 1 ~ 2”, If f is simply a type-valued function and we’re using function terminology, f Int Char evaluates to Bool.

Remember that I can put a (Assoc) Type Family call f Int Bool in a type/signature anywhere throughout the program, it doesn’t have to be within an instance decl.

Now truce: we’ll both avoid “simply” here on.

[AntC2]

@sgraf

Agda does not have a separate syntax for type classes; you simply declare a record type …

Thank you. Yeah those 'record type’s are what I’d call “practically indistinguishable” from class decls: a bunch of extra attributes that means the methods are more than ordinary functions.

What I do see in those docos is

the special module application

open Monoid {{...}} public

This will bring into scope

mempty : ∀ {a} {A : Set a} {{_ : Monoid A}} → A
_<>_   : ∀ {a} {A : Set a} {{_ : Monoid A}} → A → A → A

The open is ML-style overloading: bring into scope a specific instance. Any use of mempty within that scope is to be the Set instance irrespective of whether that’s the type demanded by the consumer. Needs a lot of bondage-and-discipline bureaucracy, is what I hear.

The “defined by hand” further down the page using Monoid.mempty is a nod to OOP style.

(Haskell-style typeclasses also need some level of bureaucracy. Particularly explicit signatures to prod the compiler into selecting the right instance. So I’m not saying better nor worse, just a different/incompatible mindset.)

[knottio]

@sgraf

Agda does not have a separate syntax for type classes; you simply declare a record type

Record types are essentially just syntactic sugar for a data type, along with a module of the same name, containing the fields and any definitions declared/opened. So while using record types is the typical way of doing type classes à la Haskell, it can be done with types defined other ways.

@AntC2

Yeah those 'record type’s are what I’d call “practically indistinguishable” from class decls

class declarations don’t define types, they define type classes (in the narrow, programming specific sense). Records define types, and in a dependent type theory, types can model type classes (in a general sense). So yeah, when you use record types to do what class declarations do, you get something “practically indistinguishable.”

@AntC2

Any use of mempty within that scope is to be the Set instance

Set is the type (or “sort”) of (“small”) types, analogous to Haskell’s *.

open Monoid {{...}} public brings mempty and _<>_ into scope with the instance argument unresolved. So if you have a file with the docs’ Monoid definition, open Monoid {{...}} public, a definition of Nat : Set, 0 : Nat and _+_ : Nat → Nat → Nat, and only the following instance declaration for Monoid Nat:

instance
  +-Monoid : Monoid Nat
  +-Monoid = record { mempty = 0; _<>_ = _+_ }

Then x = 0 <> 0 will have Agda infer x : Nat.

If you also had:

instance
  *-Monoid : Monoid Nat
  *-Monoid = record { mempty = 1; _<>_ = _*_ }

Then Agda would complain about overlapping instances, unless ran with --overlapping-instances. Off the top of my head, I don’t remember what Agda does here with overlapping instances enabled (and I don’t have access to an Agda compiler at the moment).

However, if instead of defining +-Monoid and *-Monoid within an instance block, they were just defined at the top level, then one could do open Monoid {{+-Monoid}} resulting in mempty : Nat and _<>_ : Nat → Nat → Nat in scope. One could also do x = 2 <> 3 where open Monoid {{+-Monoid}} to scope it just to the definition of x. Or there’s (assuming open Monoid {{...}}, or open Monoid {{...}} public in a module that’s been opened:

private instance
  monoidNat : Monoid Nat
  monoidNat = +-Monoid

x = 2 <> 3

@AntC2

The “defined by hand” further down the page using Monoid.mempty is a nod to OOP style.

It’s essentially just doing the following Haskell:

module Foo (mempty) where

import qualified Monoid

mempty :: _hypotheticalEquivalentToAgdaType
mempty = Monoid.mempty

In contrast with the open Monoid {{...}} public which is essentially the following Haskell:

module Foo (module Monoid) where
import Monoid

I’m guessing the “nod to OOP style” was a misunderstanding that the above should clear up. If not, I’m curious what about it is related to OOP.

[AntC2]

@knottio

when you use record types to do what class declarations do, you get something “practically indistinguishable.”

Thank you for confirming @knottio, that’s the main takeway from that part of the discussion. IOW no functional/Dependently-typed language has invented something radically different from typeclasses. (We might nit-pick with what you say, that these days Haskell’s classes are in fact types: GHCi’s :info Eq says type Eq :: * -> Constraint.)

Set is the type (or “sort”) of (“small”) types, analogous to Haskell’s *.

Errk. That is maximally confusing. I did see that Agda maintains an (infinite) hierarchy of types rather than Haskell’s Type-in-Type. Looking again at that doco page, I see both it : ∀ {a} {A : Set a} ... and elem : {A : Set} {{eqA : Eq A}} .... That seems an inconsistent usage of Set. Ok I’ll stop trying to understand Agda. Is all dependent typing as confusing as that?

instance
  +-Monoid : Monoid Nat
  ...
instance
  *-Monoid : Monoid Nat
  ...

Those aren’t merely overlapping instances, they’re identical instances, which are to be rejected in all cases. Then the only recourse in Haskell is to define some newtype over Nat, and make that an instance of Monoid. Haskell doesn’t allow private instances. (There are from time to time requests for local instances or some such. Nobody’s been able to give a coherent explanation for how that interacts with the global typeclass mechanism.)

I’m curious what about it is related to OOP.

Very likely I was/am failing to understand. It seemed to me that “defined by hand” was binding local mempty to a specific instance of Monad, not leaving it overloadable. For example, binding to +-Monad rather than *-Monad. That is, treating +-Monad as an object (in the OOP sense), and drawing some specific overloading of mempty from it, rather than resolving to the instance determined from type inference.

So I’m left puzzled: if Agda’s instance resolution is always type-driven, what’s the point of giving a name to an instance (like +-Monad)? Where would you use that name? Can you use that name to override what type inference would otherwise do?

[knottio]

@AntC2

IOW no functional/Dependently-typed language has invented something radically different from typeclasses

Not quite:

@knottio

when you use record types to do what class declarations do, you get something “practically indistinguishable.”

However, when you use the more generalized aspects of record types, you can do more than what Haskell’s class declarations can do. You can, for example, bundle the type classes’ laws within the type class, so that an instance of the type class includes not just the functions, but proof the functions satisfy the desired laws. That is radically different.

@AntC2

Errk. That is maximally confusing.

The choice to use “Set” is unfortunate, although it can now be renamed. Recent projects in Agda tend to use “Type” instead.

@AntC2

I did see that Agda maintains an (infinite) hierarchy of types rather than Haskell’s Type-in-Type.

Type-in-type with dependent types gives rise to what is more or less Russell’s paradox (“the set of all sets that aren’t members of themselves”). Stratified universes are common in set theory to resolve Russell’s paradox, and Agda does the analogous thing for its type theory.

@AntC2

it : ∀ {a} {A : Set a} ... and elem : {A : Set} {{eqA : Eq A}} .... That seems an inconsistent usage of Set

Set by itself is syntactic sugar for Set 0, so it is universe polymorphic since it’s parameterized by the Level variable a, whereas elem is not, since the {A : Set} is sugar for {A : Set 0}.

@AntC2

Ok I’ll stop trying to understand Agda. Is all dependent typing as confusing as that?

I suspect the documentation and syntax of Agda hasn’t had much feedback from people trying to learn Agda without prior knowledge of some dependent type theory, or at the very least such individuals were learning dependent type theory from other sources in tandem.

@AntC2

Those aren’t merely overlapping instances, they’re identical instances

Right, so Agda won’t be able to resolve an instance of Monoid Nat. Having both declared as instances with the same scope isn’t useful (as far as I’m aware). However, they can be declared in separate modules, and careful control of opening those modules is one way of being able to choose which instances will get resolved.

@AntC2

Can you use that name to override what type inference would otherwise do?

Yep! Since the “type constraints” in Agda are actually just types and their inhabitants, the instance resolution is used to resolve a specific inhabitant of a type, to be used as an argument to a function (or module)

The argument can be passed explicitly instead of relying on instance resolution, e.g. for a function f : {{Monoid Nat}} → Nat → Nat → Nat, one could call f {{+-Monoid}} 2 3 to have the function use 0 as the unit, and addition as the operation, or f {{*-Monoid}} 2 3 to use 1 and multiplication instead.

And for a module parameterized by an instance (such as the Monoid module), explicitly passing an instance lets you open the module with that specific instance applied. e.g. open Monoid {{+-Monoid}} brings into scope mempty and _<>_ with the instance partially applied, giving them the types Nat and Nat → Nat → Nat respectively.

Additionally, you can write a function that takes a Monoid Nat explicitly, and then pass either +-Monoid or *-Monoid as you would any other argument.

[AntC2]

@knottio

Recent projects in Agda tend to use “Type” instead.

Whew!

Type-in-type with dependent types gives rise to what is more or less Russell’s paradox

Hmm interesting. When T-in-T was introduced into Haskell, the powers-that-be were aware of the risk of undecidability. But figured there were already plenty of ways for the type/class system to be undecidable, so it wasn’t making anything worse. OTOH that was before Dependent Typing. OTOOH, a major power-that-be had already written their thesis all about DT in Haskell. So I’m bemused.

Set by itself is syntactic sugar for Set 0

If I might critique that of which I know nothing, that seems totally cr*p design: any constructor can be partially applied. In higher-order typing, aren’t there contexts (constructor classes?) where you want (unapplied) Set to be an argument to a fancy doo-hickey?

I suspect the documentation and syntax of Agda hasn’t had much feedback from people trying to learn Agda without prior knowledge of some dependent type theory, …

I have looked at endless tutorials on Dependent Type theory. They’ve failed to resonate with me in any usable way. (Or perhaps I mean I’ve failed to resonate with them.) Then I was reading the Agda docos in the hope of more practical material. Clearly I’m mentally incompetent. Wise of me to just keep away from Haskell here on.

they can be declared in separate modules, and careful control of opening those modules is one way of being able to choose which instances will get resolved.

That sounds dangerously like ‘orphan instances’. Nobody’s been able to bring an example where that causes actual incoherence/segfaults. OTOH it regularly gives perplexing behaviour. so GHC gives warnings if it suspects that’s happening. The language standard is written on the basis all instances are visible at all times.

What you go on to say “The argument can be passed explicitly instead of relying on instance resolution, …” sounds like
a) at least a “radically different” way to use typeclasses/instances [**], even if a fairly familiar way to declare them;
b) an excellent source for hard-to diagnose overloading behaviour; in particular
c) an awkward way to interact with Agda’s equivalent of Functional Dependencies (presumably type-level functions needing instance resolution).

Thank you for all your help (trying to) unconfuse me. I suspect I’m a hopeless case.

[**] Addit: we-ell you could contrive Haskell to kinda sorta mimic that usage. A module with the NatPlusMonad instance; a module with NatTimesMonad. Be very careful to never import them both into the same place. That’ll be really difficult because of the likelihood of transitive imports.

[atravers]

@tomjaguarpaw

It’s hard to summarize how I feel about generators, but maybe this does the job: “generators are often complicated enough to themselves need tests”.

Alternatively:

• a practical test should not require its own tests

because of the risk of infinite indeterminate regress:

• test1 needs test2 which needs test3 which needs test4 which needs …

which isn’t practical.

Similarly:

• a practical type system should not require its own type system

because there really is an infinite hierarchy of types!

Trying to solve the problems in one type system by introducing another type system makes as much sense as:

• trying to solve the problems in one test by introducing another test;

• trying to solve the problems in one testsuite by introducing another testsuite.

Adding more tests, testsuites, and type systems means more code, and more code means more bugs.

[AntC2]

@atravers

introducing another type system

Does Dependent Haskell embody “another” type system? Or is it an (allegedly) easier to grok mechanism to replace FunDeps, (Assoc) Type Families, awkwardness with signatures needing binding and scoping of tyvars? [Genuine questions: I don’t know.]

Or is there to be a two-tier Haskell?: those writing the compiler and core libraries speak the language of the priesthood; stupid Haskellers (like me) merely use those libraries, aren’t expected to write infrastructure-level code, so don’t need to deal with exotic types. [I have a wee suspicion they’ll still see obscure type-riddled error messages.] To repeat a point from above: it’ll all be out of sight behind extensions.

[atravers]

Does Dependent Haskell embody “another” type system?

Here’s a simpler question: do dependent types require “another” type system?

For the curious reader I encourage you to look at PolyKinds and TypeFamilies, these let you express some very sophisticated programs at the type level in Haskell. If this really tickles your fancy, perhaps make the leap to Agda, Idris, or Coq to enjoy full dependent types.

C&C - Types and Kinds and Sorts, Oh My!

So if Haskell is (currently) “poor man’s Agda”…I would say yes.

Before TypeInType arrived in GHC, kinds were the “type” of types and sorts were the “type” of kinds. So in addition to the type and kind systems, GHC also had a sort system.

As for Agda:

Sorts (also known as universes) are types whose members themselves are again types. The fundamental sort in Agda is named Set and it denotes the universe of small types.

Sort System — Agda 2.7.0.1 documentation

---

I have a wee suspicion they’ll still see obscure type-riddled error messages.

It won’t only be error messages:

#  ghci -XHaskell2010
GHCi, version 9.8.2: https://www.haskell.org/ghc/  :? for help
ghci> :t case getChar of IO a -> a

<interactive>:1:17: error: [GHC-76037]
    Not in scope: data constructor ‘IO’
ghci>
ghci> :i IO
type IO :: * -> *
newtype IO a                                                       -- None of
  = GHC.Types.IO (GHC.Prim.State# GHC.Prim.RealWorld               -- this should
                  -> (# GHC.Prim.State# GHC.Prim.RealWorld, a #))  -- be visible in
  	-- Defined in ‘GHC.Types’                                      -- Haskell-2010 mode
instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’
instance Semigroup a => Semigroup (IO a) -- Defined in ‘GHC.Base’
instance Applicative IO -- Defined in ‘GHC.Base’
instance Functor IO -- Defined in ‘GHC.Base’
instance MonadFail IO -- Defined in ‘Control.Monad.Fail’
instance Monad IO -- Defined in ‘GHC.Base’
ghci>

• (page 95 of 329)

  The IO type serves as a tag for operations (actions) that interact with the outside world. The IO type is abstract: no constructors are visible to the user. IO is an instance of the Monad and Functor classes.

  The Haskell 2010 Report (emphasis added)

[knottio]

@AntC2

aren’t there contexts (constructor classes?) where you want (unapplied) Set to be an argument to a fancy doo-hickey?

(a : Level) → Set a is what Set would be if it wasn’t overridden by syntactic sugar. So you could give that a name, e.g. Set' = (a : Level) → Set a and use Set', but people generally just write (a : Level) → Set a out in full, especially since you often need to give the level a name, anyway. Regardless, I don’t think I’ve ever written a type where I could actually use Set', since usually you want something like (a : Level) → Set a → ... not ((a : Level) → Set a) -> ... and Set' → ... would be the latter.

@AntC2

I have looked at endless tutorials on Dependent Type theory. They’ve failed to resonate with me in any usable way.

I suspect the learning curve for dependent types is fairly front-loaded; requiring you to learn a lot very early on, with seemly no gain, then suddenly new concepts come much more easily when presented using the dependently typed fundamentals. Seems similar to category theory in that regard. How true that is remains to be seen.

@AntC2

That sounds dangerously like ‘orphan instances’.

I’m not familiar with the intricacies of orphan instances. From what I skimmed from the Haskell wiki, it seems it isn’t applicable in Agda because Agda has private instances, and has --no-qualified-instances which allows using a module with a public instance without Agda considering the instance for resolution.

@AntC2

he argument can be passed explicitly instead of relying on instance resolution, …” sounds like
a) at least a “radically different” way to use typeclasses/instances

I suppose it would make more sense to talk about parametric vs ad-hoc polymorphism here. In Haskell, if you wanted to do “type classes” parametrically, you would do e.g.:

-- defining Monoid for parametric polymorphism
data Monoid' a = Monoid' { mempty' :: a, mappend' :: a -> a -> a }

-- defining a new function parameterized by a Monoid
mconcat' :: Monoid' a -> [a] -> a
mconcat' mon = foldr (mappend' mon) (mempty' mon)

-- defining an "instance" of Monoid
listMonoid :: Monoid' [a]
listMonoid = Monoid' [] (++)

-- using a function with Monoid parametrically
x = mconcat' listMonoid [ [ 0 ] ]

vs. the ad-hoc polymorphism of e.g.:

-- defining Monoid for ad-hoc polymorphism
class Monoid a where
  mempty :: a
  mappend :: a -> a -> a

-- defining new function with a Monoid constraint
mconcat :: Monoid a => [a] -> a
mconcat = foldr mappend mempty

-- defining an instance of Monoid
instance Monoid [a] where
        mempty  = []
        mconcat = (++)

-- using a function with Monoid ad-hoc
x = mconcat [ [ 0 ] ]

But in Agda, when defining Monoid, you don’t have to make a choice of parametric vs ad-hoc; you can make the choice when using Monoid, instead:

-- defining a Monoid for ad-hoc AND parametric polymorphism
record Monoid (a : Set) : Set where
  field
    mempty : a
    mappend : a -> a -> a
open Monoid {{...}} public

-- defining a new function parameterized by a Monoid, as an instance argument
mconcat : {a} -> {{Monoid a}} -> List a -> a
mconcat = foldr mappend mempty

-- defining an instance of Monoid
instance
  listMonoid : {a} -> Monoid (List a)
  listMonoid = record { mempty = []; mappend = _++_ }

-- using a function with Monoid ad-hoc
xAdhoc = mconcat [ [ 0 ] ]

-- using a function with Monoid parametrically
xPara = mconcat {{listMonoid}} [ [ 0 ] ]

With this one definition, you can use Monoid ad-hoc by using it like you would a type class in Haskell, e.g. mconcat [ [ 0 ] ] (assuming an appropriate instance available), or you can use it like you would in the parametric Haskell version above (e.g. Haskell: mconcat listMonoid [ [ 0 ] ]) except the Monoid argument is surrounded by double braces, e.g. mconcat {{listMonoid}} [ [ 0 ] ].

So it’s less “using typeclasses in a radically different way” and more “using parametric polymorphism when it’s more appropriate than ad-hoc, without requiring separate ad-hoc and parametric implementations”.

@AntC2

an excellent source for hard-to diagnose overloading behaviour

I don’t know what “overloading behaviour” refers to here.

@AntC2

Or is there to be a two-tier Haskell?: those writing the compiler and core libraries speak the language of the priesthood; stupid Haskellers (like me) merely use those libraries, aren’t expected to write infrastructure-level code, so don’t need to deal with exotic types

Reminds me of type level programming in TypeScript. Some libraries will use black magic advanced type definitions to better constrain valid vs invalid inputs; often at the cost of impenetrable type errors. Similarly, in Agda, inspecting type holes in an algebra 101 proof involving the stdlib rational numbers can easily result in displaying a single type take takes up your whole screen. Although I’ve heard that’s been improved a bit recently.

@atravers

Adding more tests, testsuites, and type systems means more code, and more code means more bugs.

Likewise, adding more data redundancy means more data, and more data means more data corruption. Hence why I don’t backup any of my data: it increases the likelihood of corruption! Instead, I store my data long term with maximal compression to reduce its footprint.

[atravers]

[…] more data means more data corruption.

Here’s some decades-old data:

https://pds-geosciences.wustl.edu/missions/magellan/index.htm

and here’s some decades-old code:

https://web.archive.org/web/20240920070532/https://ftp.gwdg.de/pub/languages/funet.fi/ml/lml/

(I’ll let you decide which one is more difficult to use after all that time ;-)

---

@knottio

[…] I don’t backup any of my data: it increases the likelihood of corruption! Instead, I store my data long term with maximal compression to reduce its footprint.

Best file compression around: "rm *.*" = 100% compression

Mike DeMaria

---

Having three copies of data is different from having three levels of types:

• If only one data copy has errors, either of the other two copies will suffice (redundancy).

• But if only one type system has errors, it can affect the entire program (no redundancy).

[AntC2]

@atravers

express some very sophisticated programs at the type level in Haskell.

That was written 2014, rather a long time after Oleg’s work, which included IIRC a Sudoku solver written entirely within the type system, chiefly to demonstrate how compile-time is Turing-complete. I am not claiming that work is easy to follow.

Then I’m unimpressed by what I’ve seen so far of Dependent Haskell (or Agda), because it seems to add an awful lot of ugly syntax, to achieve no more than I (or rather Oleg) can already [**]. Note Oleg originally used only FunDeps, not even Type Families, nor DataKinds.

kinds were the “type” of types and sorts were the “type” of kinds. So in addition to the type and kind systems, GHC also had a sort system.

This wasn’t specific to GHC. Haskell 98 Language report, section 4.1.1 Kinds

unlike types, kinds are entirely implicit and are not a visible part of the language.

So it’s the language that already has a kind system (and even more shadowy sort system). Then to answer the question at hand: no, Dependent Haskell isn’t adding “another” layer. What GHC provided was to make it more visible so you can write kind signatures. (They’re useful documentation, but not essential: the compiler can infer kinds from the type sig. You can set an option in Hugs to see Kind signatures.)

Distinguishing terms vs types vs kinds is what allows punning, including that kind * is distinct from term (*). And this doesn’t give rise to ambiguity because to the left of :: is a different namespace to its right (is different to the right of a :: nested on rhs of ::). It all works rather elegantly IMHO. DataKinds and then Type-in-type is the slippery slope to: allowing types in terms with no syntactic herald is an act of vandalism.

[**] Beware a few type-level extensions were taken out of GHC sometime after 2006, meaning you nowadays are forced to use the ugly syntax.

[atravers]

Here’s one difference between kinds in Haskell 98 and (pre-TypeInType) GHC:

polymorphic kinds · Wiki · Glasgow Haskell Compiler / GHC · GitLab

So the fragment of a kind system that was in Haskell 98 was getting closer and closer to being another fully-formed “type” system in GHC. And if it weren’t for the TypeInType extension, the same would have eventually happened for the fragment of the sort system that was in Haskell 98.

It’s a perpetual cycle:

1. System_N for "types"_N is developed;

2. Over time, system_N acquires fragments of system_{N +1} to accommodate more features for "types"_N.

3. As a result of that ongoing expansion, the problems that had appeared in system_N begin to re-appear in system_{N +1}.

4. (Increment N by one, then go back to step 1.)

So how many more times does this cycle have to be repeated before everyone realises that the result after each time will always be the same - to infinity and beyond?

[AntC2]

@knottio

I’m not familiar with the intricacies of orphan instances. From what I skimmed from the Haskell wiki, it seems it isn’t applicable in Agda because Agda has private instances,

Yes, fair comment. Haskell doesn’t support private instances in any way. Even if you tried to contrive them with cunning use of the module/import system, the compiler would probably defeat you. (“orphan instances” is the effect of applying within one module an instance which the compiler wouldn’t choose for exactly the same code if it could see all instances where this module is going to get imported into.)

In Haskell, if you wanted to do “type classes” parametrically,

I’m pretty sure that won’t scale:

• do notation insists on the standard names for Monadic operations;
• classes are arranged in hierarchies, with Laws to bind between them. (class Semigroup a => Monoid a ..., class Applicative m => Monad m, class Functor f => Applicative f, … aka ‘the Jenga tower’).
• Then you can’t define just one or two parametric methods; you’d need parametric versions for the whole Prelude. And with explicit linkages up the hierarchy.
• “hard-to-diagnose overloading behaviour” would then be figuring out whether your program parametrically chose an instance vs ad-hoc inferred, and whether that was what you intended.

(As I said above, not better nor worse, just confusingly different.)

[knottio]

@AntC2

I’m pretty sure that won’t scale:

I don’t mean to imply that doing the “type classes parametrically” is a good idea in Haskell. It was just to contrast to Agda’s “type class” approach, demonstrating that Agda’s approach works both parametrically and ad-hoc, doing the same two things done in Haskell, just without having to choose between the two. It scales fine because it’s just one approach that does both, rather than two separate approaches that step on each other’s toes.

@atravers

As a result of that ongoing expansion, the problems that had appeared in systemN begin to re-appear in systemN +1.

If introducing system_{N +1} means my codebase of 100% system_N becomes 90% system_N and 10% system_{N +1} and it gets rid of problems from system_N but system_{N +1} has those problems, then I removed those problems from 90% of my codebase.

Given you’re on a Haskell forum, presumably you find value in a type system for your values. So why not a type system for your type system? Even if you have reasons for the former and not the latter, it can’t just be “more code” because (presumably) you find the value of the former to be worth the “more code” that it requires.

@atravers

(no redundancy).

If I write an error at value level, but my type level declaration is correct (and applicable to the error), I catch the bug. If my type level declaration also has an error, but my type’s type level declaration is correct (and applicable to the error), I catch the bug. Sounds like redundancy to me.

[atravers]

If introducing system_{N +1} means my codebase of 100% systemN becomes 90% system_N and 10% system_{N +1} and it gets rid of problems from system_N but system_{N +1} has those problems, then I removed those problems from 90% of my codebase.

“Type” system level	fraction of errors not found
1	10% (0.1)
2	1% (0.12 = 0.01)
3	0.1%
4	0.01%

…therefore no matter how many levels there are, some bugs will always remain undetected. So again:

@atravers

[…] how many more times does this cycle have to be repeated before everyone realises that the result after each time will always be the same […]

---

If I write an error at value level, but my type level declaration is correct (and applicable to the error), I catch the bug. If my type level declaration also has an error, but my type’s type level declaration is correct (and applicable to the error), I catch the bug.

…which I’ll rewrite as:

• If you write an error at value level, but your type_N -level declaration is correct (and applicable to the error), you catch the bug.

• If your type_N -level declaration also has an error, but your type_N’s type_{N +1} -level declaration is correct (and applicable to the error), you catch the bug.

  @atravers

  […] to infinity and beyond?

---

Sounds like redundancy to me.

Here’s the definition of “redundancy” I’m relying on:

redundancy noun [C or U] (NOT NEEDED)

a situation in which something is unnecessary because it is more than is needed:

• The aircraft has seven computer systems running in parallel, so as to provide enough redundancy to cope with computer breakdowns.

REDUNDANCY | English meaning - Cambridge Dictionary

But if you have a tower of N -1 sufficiently-featured type systems and the fragments of one more, then the loss of only one type system is enough for source-code bugs to be missed. Therefore the entire tower has to work! Or using the avionics example, all of the computers must work for the aircraft to keep flying safely (no redundancy).

Fortunately, aircraft everywhere use the dictionary definition of “redundancy” for their avionic systems - if only one system fails, the pilots probably still can land their aircraft safely.

---

Given you’re on a Haskell forum, presumably you find value in a type system for your values.

Conditionally - I also agree with the concept of diminishing returns, with a bemusing example provided by roundabouts; this being an ordinary one:

(source)

But why stop there?

(source)

That’s a “roundabout of roundabouts” - five small ones arranged in a loop (appearing as white dots amongst the vehicles) around a large one in the middle (the white dot in the middle of the central circular area). As you can now probably understand, there are very few of these anywhere in the world: going beyond a single roundabout at an intersection of roads provides diminishing returns, but so much added complexity, and extra “fun” for learner-drivers!

@atravers

So instead of adding dependent types to the last remaining widely-supported non-strict language, make Agda into another non-strict language with similar support - if lazy Agda fails, at least there’ll still be non-dependent Haskell…

[atravers]

@int-index

I’ve been working on a task breakdown that I intend to publish by the end of this year.

As it stands, my draft for that page has 18 completed milestones, 5 ready for implementation, and 20 that are yet to be discussed and refined.

That’s in rather broad strokes – I expect to break it into smaller subtasks over time.

So far this topic has attracted over 200 “likes”, mostly for “pro-DT” posts. So if even 10% of those individual “likers” (approximately 20 people) were to join int-index and sand-witch in this experiment, we (including Haskell educators and practitioners) will all be able to see the results that much faster.

Why the emphasis on educators and practitioners? Because we want more people using Haskell, not less:

• educators teaching more students Haskell, who then go on to be practitioners;

• practitioners advocating for the use of Haskell, including to prospective students.

So by it arriving more quickly, we’ll have the opinions of educators and practitioners about a “dependent Haskell” that much sooner, and know if this experiment is a success (or not) and respond accordingly.

[knottio]

@atravers

then the loss of only one type system is enough for source-code bugs to be missed. Therefore the entire tower has to work! Or using the

Identifying an instance in which something isn’t redundant doesn’t invalidate the ways in which it is.

@atravers

I also agree with the concept of diminishing returns…

Yes, diminishing returns of course mean that at some point, going further stops being worthwhile. This is an extremely well understood concept. Pointing out the existence of diminishing returns contributes nothing towards the actual difficult part: finding when it is no longer worthwhile.