The future of Dependent Haskell

[atravers]

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

But it does invalidate your counter-example of data corruption:

@atravers

• 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).

---

Pointing out the existence of diminishing returns contributes nothing towards the actual difficult part: finding when it is no longer worthwhile.

The future of Dependent Haskell

Here’s one possibility: universities, colleges and other centres of education decide to switch their curricula away from a “dependent Haskell” and its perceived-as-too-steep “learning curve” to a combination of: Prolog (logic, laziness); Erlang (functional, Prolog-based syntax). with “dependent Haskell” possibly being relegated to an advanced-theory course (but with education budgets getting ever-tighter…that isn’t guaranteed either).

If new features and extensions for Haskell tend to benefit experienced users (such as implementors of Haskell) at the expense of making Haskell more difficult to teach, or advocate to future Haskellers, then there simply will be less Haskellers in the future.

So will dependent types be one such addition? I don’t know. Hence me referring to their addition to Haskell as an experiment, and me wanting to know what happens next if that experiment fails since failure is always an option for any experiment:

@atravers

data Risk a b = Loss a | Gain b

…and choosing to think wishfully about the risk of failure does exactly nothing to lessen or remove it.

But we’ll all discover if it is a failure or not much more quickly if more people help int-index and sand-witch…

[AntC2]

@atravers

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.

Now hang on. DataKinds arrived 2012. Are we saying that also counts in Dependent Haskell? Then when did DepH start? And what type-system extensions in Haskell post-98 count as non-DepH? We’re losing focus. I think I can be in favour of DataKinds without swallowing the whole DepH kool-aid.

@knottio

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?

Given GHC’s type system as at 2010, what would be far more valuable to deliver next would be a type system to catch divide-by-zero or numeric overflow or off-by-one errors. A type system for my type system not so much of a priority. (And writing a PolyKinded Typeable to save a handful of different arity Typeables strikes me as thin motivation.)

Note that Oleg’s work used the type system as at 2004. DataKinds are more elegant, but no more expressive than 2004. Note also that Hugs’ extensible records system (TRex ~1996) exploits the implicit kind system (row is a different kind vs *) without anyone needing to write explicit kind signatures. Has GHC three decades on produced a record system? Is DepH going to enable me to produce one? Lenses requires a vast amount of eye-watering code (and was also delivered before DepH – will DepH help Lenses avoid all that Template Haskell?).

@atravers

2. Over time, systemN acquires fragments of systemN +1 to accommodate more features for “types” N.

I suspect there are a smaller and smaller set of applicable fragments as you go up the hierarchy. So perhaps it’s reasonable for Agda to leave the levels explicit. I note the violence DepH is doing to Haskell to be able to put types in terms. I suspect there’ll be more violence when it comes to writing type-level functions, because of all the syntax from term-level that doesn’t make sense at type-level. IOW when you write a function, you’ll have to know whether this is to be called at levelN vs levelN+1 etc. So the terms vs types vs kinds vs sorts distinction will reappear.

For example: do typeclasses/overloading make sense at the kind level? instance Eq Type ... anyone? Merely testing for the equality of two types without signalling to type inference these types are unifiable will lead to a healthy new source of bugs. if (type a) == (type b) then ... else .... I’d be especially interested in what dragons we can find in the else ... branch.

[atravers]

Now hang on. DataKinds arrived 2012. Are we saying that also counts in Dependent Haskell? Then when did DepH start?

Notice my use of the word “fragments” with regards to the use of “higher” type systems - all “printed” versions of Haskell (from version 1.0 through to 98 and 2010) rely on such artefacts, namely the kind and sort system fragments mentioned here:

https://jozefg.bitbucket.io/posts/2014-02-10-types-kinds-and-sorts.html

By themselves those fragments are relatively benign. Instead, the risk arises from their ongoing extension - what was a fragment now begins to resemble a whole extra type system, with all of the usual problems any type system has. Hence step 3 of that perpetual cycle:

@atravers

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.)

[knottio]

@atravers

• 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).

If all three copies are on a device that are exposed to a fire, no copies remain. So, does that mean “no redundancy”? Of course not, because:

@knottio

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

@atravers

But we’ll all discover if it is a failure or not much more quickly if more people help int-index and sand-witch…

Indeed, if people interested in discovering such a thing, perhaps such as those posting about what’s going to happen as a result of Dependent Haskell, were to help work on it, those individuals would find out faster than if they were (say) speculating on it instead.

@AntC2

what would be far more valuable to deliver next would be a type system to catch divide-by-zero or numeric overflow or off-by-one errors

Are there established ways of doing that, just waiting to be implemented? Is the implementation of Dependent Haskell delaying that? (I genuinely don’t know.) I do know that dependent types provide some means of doing so, albeit established methods have limits and trade-offs (as all things do). Are there established means of doing it better without dependent types?

@AntC2

instance Eq Type

In Agda, the only two possible implementations of an instance of Eq Type are (==) _ _ = False and (==) _ _ = True (Type has no constructors, so nothing to pattern match on), neither of which seem particularly useful. Regardless, if implemented, your example of if (type a) == (type b) then ... else ... would just reduce to either if True .. or if False .... I don’t see the problem; would Dependent Haskell do something differently here?

@AntC2

all the syntax from term-level that doesn’t make sense at type-level.

@AntC2

when you write a function, you’ll have to know whether this is to be called at levelN vs levelN+1

Can you give examples of these?

[AntC2]

@knottio

Are there established ways of doing that [catch numeric invalid values], just waiting to be implemented? …

The current best effort AFAIK is Liquid Haskell.

… Is the implementation of Dependent Haskell delaying that? (I genuinely don’t know.)

I guess you wouldn’t want to be implementing both at the same time into the same compiler. They’ll be trampling over each other. Also resourcing: there’s only a handful of people understand enough of GHC’s internals. OTOH at least one of that handful has expressed (up-thread) they’re interested only in Dependent Typing. So (as with many bright ideas for Haskell) an officially integrated LH-alike will probably never happen.

I do know that dependent types provide some means of doing so, albeit established methods have limits and trade-offs (as all things do).

I guess (and I am guessing) the DepT approach would be to convert an Int to Peano Numerals, to give a structure to walk through. And we’d have to express numeric operations in terms of Peano Axioms. I suspect this would give the opposite of human-readable code.

Are there established means of doing it better without dependent types?

LH uses an SMT solver. That feels like a much more appropriate tool.

In Agda, the only two possible implementations of an instance of Eq Type

I think you’re failing to grok higher-order typing. For instance Eq Int ..., the operands for (==) are numbers – that is elements of the set of Ints. Then for instance Eq Type ... (about which I am not being serious – but it’s why this isn’t serious that’s at question), the operands for (==) would be Types – that is Int, Bool, Char, (Maybe String), [Float], .... So an example of syntax at one level that doesn’t make sense at a different level:

foo :: forall a b. a -> b -> Bool
foo @a @b (x :: a) (y :: b) = if (type a) == (type b) then x == y else False
--  ^^ type of foo's first argument
--     ^^ type of foo's second argument

It doesn’t make sense because the x == y requires we already have proof the operands are same type; whereas (type a) == (type b) is merely a Boolean expression not furnishing any proof.

I am being very careful in that example to put the explicit (type a) herald. Dependentistas frown on this/it’s for the weak-minded, they put (and this has just arrived in 9.12) bare a, b. Then for the casual reader there’s scant clue this is Dependently-typed code.

I would like to say the “type system for our type system” would reject any attempt to declare instance Eq Type ... because Type is an … errrm … kind …, not a type, and Eq :: Type -> Constraint. But we have Type-in-Type so I’m no longer allowed to use “kind”. Then AFAICT Type is a Type and eligible for an instance Eq. And indeed GHC (8.10) just let me do that. Now I’m scared for my sanity.

[atravers]

@knottio

If all three copies are on a device that are exposed to a fire, no copies remain.

That’s why you should have copies on at least three separate devices, with at least one of those devices in a separate location:

Grandfather-father-son backup scheme

---

@knottio

Indeed, if people interested in discovering such a thing […]

Such as yourself? Then you can join in the fun once int-index publishes that task-breakdown page ;-D

---

@AntC2

foo :: forall a b. a -> b -> Bool
foo @a @b (x :: a) (y :: b) = if (type a) == (type b) then x == y else False

This is somewhat reminiscent of Ohmu:

(page 80 of 300)

3.2 Computations with Prototypes

Treating values as types has some interesting consequences. First of all, it means that values and types must have the exact same interface. In other words, if it is possible to evaluate an expression like (3 + 1), it must also be possible to evaluate the expression (Integer + 1). If this were not true, then replacing Integer with 3 would not be a type-safe operation.

[rhendric]

@AntC2

So an example of syntax at one level that doesn’t make sense at a different level:

foo :: forall a b. a -> b -> Bool
foo @a @b (x :: a) (y :: b) = if (type a) == (type b) then x == y else False
--  ^^ type of foo's first argument
--     ^^ type of foo's second argument

I don’t really follow what this example function has to do with the point you hope to make about type-level classes—there are other reasons why instance Eq Type is not something one should reasonably expect to have, but this function when given the correct constraints can be correctly written today, no problem:

{-# LANGUAGE GADTs, TypeAbstractions #-}

import Data.Typeable

foo :: forall a b. (Typeable a, Typeable b, Eq a) => a -> b -> Bool
foo @a @b (x :: a) (y :: b) = case eqT @a @b of
  Nothing -> False
  Just Refl -> x == y

No DH here, just GADTs, Typeable, and library-level propositional equality. Maybe you get off the GHC bus before the GADTs or Typeable stops though?

[AntC2]

@rhendric

No DH here

Quite. And thank you for that code. It’s ugliness does tell this casual reader there’s some fancy type-manipulation going on. Entirely appropriate.

instance Eq Type is not something one should reasonably expect to have,

I don’t expect to have it. I think it’s entirely unreasonable. But GHC (8.10) just let me declare that instance. If TypeinType is supposed to be such a Good Thing, please explain why that instance isn’t an outright error that GHC should reject.

Maybe you get off the GHC bus before the GADTs or Typeable stops though?

Typeable dates to before 2006. I’d write that code using a TypeEq class, with overlapping instances (and probably a FunDep), also available before 2006. So same-same. Don’t need no stinkin’ Dependent Haskell, as you say.

[rhendric]

@AntC2

I don’t expect to have it. I think it’s entirely unreasonable. But GHC (8.10) just let me declare that instance. If TypeinType is supposed to be such a Good Thing, please explain why that instance isn’t an outright error that GHC should reject.

It’s more that I don’t see much of a distinction between that and instance Eq (IO a), which is also quite an unreasonable thing to have, but which you can also write without outright errors.

[knottio]

@AntC2

The current best effort AFAIK is Liquid Haskell.

What’s missing from Liquid Haskell that would be afforded by integrating it into GHC?

@AntC2

It doesn’t make sense because the x == y requires we already have proof the operands are same type; whereas (type a) == (type b) is merely a Boolean expression not furnishing any proof.

What does the (type a) == (type b) have anything to do with trying to do x == y? How is this any different from if True then x == y else False? If the Haskell type checker rejects if True then x == y else False because it doesn’t have evidence a and b are identical, then why wouldn’t it reject if (type a) == (type b) then x == y else False, too?

@AntC2

I would like to say the “type system for our type system” would reject any attempt to declare instance Eq Type ...

The Agda equivalent to instance Eq Type doesn’t reject it, and Agda’s type system is (presumable) sound (in this regard). I gave 2 totally valid Agda instances of Eq Type in my post, and I don’t see why they wouldn’t also be just as valid in Dependent Haskell. Eq Type is the class of equivalence relations on Type. This is just as valid as e.g. data Empty deriving (Eq).^[1]

[1]: Not actually true. See this reply. What’s written before the strikethrough is technically correct, though.

[rhendric]

@knottio

This is just as valid as e.g. data Empty deriving (Eq).

Well, not to overly nitpick what is otherwise a lot of good sense coming out of you, but in Haskell at least instances of Eq are strongly encouraged to satisfy reflexivity and extensionality, which for instance Eq Type rule out eq _ _ = False and eq _ _ = True respectively (the latter case assuming we get Π-functions to discriminate between types). instance Eq Empty trivially satisfies both.

[knottio]

Oh, right! Definitely not a nitpick; I even wrote "Eq Type is the class of equivalence relations on Type" in my post, which isn’t actually true due to extentionality.

This is actually a nice example of the utility of dependent types, though. Instead of

class Eq a where
  (==) :: a -> a -> Bool

it could be (hypothetical syntax):

class Eq a where
  (==) :: a -> a -> Bool
  eqRefl :: (x :: a) -> (x == x) :~: True
  -- TODO eqSym, eqTrans, eqExt, etc.

And then Eq Type would be uninhabited, so instance Eq Type would effectively be a type error, just as AntC2 wants. And with that, I wouldn’t have missed the laws when I checked that instance Eq Type where (==) _ _ = True is valid.

[AntC2]

@knottio

I gave 2 totally valid Agda instances of Eq Type in my post, and I don’t see why they wouldn’t also be just as valid in Dependent Haskell.

Either of those instances (but not both together) are accepted in pre-Dependent Haskell. Thank you to @rhendric for pointing out the Law-breaking.

@rhendric

distinction between that and instance Eq (IO a)

To keep with the logic-chopping (and apologies for introducing another word in the space of type/kind/sort/…) I’d call instance Eq Type ... a ‘category mistake’. Eq applies for types inhabited by values/expressed as terms. Before TypeinType I’d say 'of kind *', and note that instance Eq * ... is invalid syntax, so more egregious than instance Eq (IO a) .... If the explanation in terms of breaking reflexivity/extensionality [**] works for you, that’s also good. For the same reason, Haskell discourages Eq over functions, because the compiler can’t verify reflexivity/extensionality [***].

@knottio

This is actually a nice example of the utility of dependent types, though.

The arguments for DepT are full of this sort of sophistry: we’ve set up some aerated feature that allows expressing arrant nonsense. So now we can call up some convoluted syntax to tame the beast/go round the houses to end up where we were already. I still haven’t seen examples that deliver functionality beyond what was already possible ~2006. It might be the code is more succinct or elegant – that’s an aesthetic judgment – but only if you’re happy with type annotations everywhere. I rather thought the merit of Haskell/Hindley-Milner is we don’t need so many type annotations, like dumb-ass languages such as C, ALGOL, Fortran, COBOL, Java, …

[**] That is, the only way to write a method overloading is with wildcard _ == _ = <constant>

[***] BTW instance Eq (Type -> Type) where _ == _ = False also accepted.

[AntC2]

@knottio

What’s missing from Liquid Haskell that would be afforded by integrating it into GHC?

Currently LH is expressed in what are comments syntactically, needing a pre-processor to find them. I believe this also means editor tools can’t validate the code dynamically. The LH type annotations are not treated as part of Haskell’s type system.

[knottio]

@AntC2

I’d call instance Eq Type ... a ‘category mistake’.

What about it doesn’t make sense? The example you gave earlier about why it was nonsense seems to have been incorrect, so I still don’t know what it is about an instance of Eq Type you object to.

[f-a]

The thread had an interesting discussion but now is a back and forth among a handful of people, and it is very difficult to follow from start to finish as it started two months ago and has more then one hundred messages (I admit not having read all of it).

To all participants: please consider opening a new discussion(s), self-contained and of smaller scope.

[AntC2]

@knottio

what it is about an instance of Eq Type you object to

Because GHC now has TypeinType, I’m not able to state the objection in today’s terminology. So let me revert to H98 terminology of value/type/kind/sort. If I ask Hugs (as using terminology closest to H98) or GHC v8.10 set to avoid TinT as far as possible:

Hugs>> :info Functor           -- and similar response for Monad
-- constructor class with arity * -> *
Hugs>> :info Eq                -- and similar response for Num
-- type class
GHCi>> :info 
type Functor :: (* -> *) -> Constraint
type Eq :: * -> Constraint

(I’m taking Hugs’ bare type class to mean with arity *.) Then instance Functor expects as argument a one-place type constructor; instance Eq expects a type constructor with kind * (which is how Hugs describes Bool, Int, ...).

* is not a type constructor, it’s a kind. So an attempted instance Eq * gets rejected because Syntax error in input (unexpected symbol "*"). IOW * is a symbol in the kind namespace, not a type constructor. Contrast attempted instance Eq Maybe rejected Kind error in class constraint. Compare GHC rejects Expected a type, but 'Maybe' has kind '* -> *'.

I guess in this Brave New World, somebody might want some class to be PolyKinded (like Typeable). But Eq is not that class; so I want attempted instance Eq * ... or Eq Type to be rejected as ill-kinded/or illegal syntax.

(Doesn’t this make sense in Agda’s levels? The argument to instance Eq must be a Set 0.)

[hellwolf]

By this rate, by the end of 2024, we might have a book coming out from all these references and texts contributed. The only thing missing is an abstract of what it is trying to convey and who are the target audience.