Hacker News Reader

Comment by dnomad | Hacker News Reader

It's not clear that dependent types even are types. Does a zero-length list offer a different methods than a list that contains some elements? Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements?

The entire domain is highly dubious and the people researching it are often of ill repute.

View on HN

c.f. https://github.com/deech/LeftPad/blob/master/left-pad.org , in particular "At the type level we have:" and "At the level of sorts and refinements:"

Or take this silly code: https://stackoverflow.com/questions/50658528/how-do-you-repl...

At the type level, nothing changes between the first program and the second. At the level of sorts and refinements, ATS2 is given more information in the second program so it's able to turn the two noted error conditions into compile time errors, when in first program they could only be runtime errors.

I haven't heard anything bad about Hongwei Xi. Who are these ill-regarded researchers?

Basically, the way it works is that the compiler prevents you from calling functions like head, tail and remove unless it has a proof that the list is non-empty.

Well, how are you defining type?

Are you defining type by the collection of methods a value or term of that type would have? That doesn't seem like the best definition to me, but ok.

I would think that a good definition would probably involve something like, a type is the thing which restricts what terms or values can be in what places in what expressions/statements.

As others have said, a function could very well require that its argument be a list which isn't of length 0.

The way you phrased the question sounds like you are thinking of the methods as being contained in the value or something like that. Things don't need to work that way.

You could just treat "calling a method" of an object like a different notation for calling a function with that object being the first argument.

(Which, if the method required the list to be non-empty, would just be a compile time type error if it couldn't be determined that the list would be non-empty.)

> Does the compiler magically...

No. There is no magic. I had trouble understanding dependent types at first, thinking that the compiler was doing something magical, but in fact it's excrutiatingly simple (it has to be, since computers are dumb).

> It's not clear that dependent types even are types.

In the case of lists and non-empty lists, these can indeed be represented as different types. In particular, a non-empty list is a pair type, containing a value and a list of values, e.g. `(myInt, myListOfInts)`. This represents a non-empty list starting with `myInt` and followed by whatever's in `myListOfInts`. Notice that this must be non-empty, regardless of what's in `myListOfInts` (or if it's empty), since we have the first value right there (`myInt`)!

This is a fundamentally different type than a normal, potentially empty list. Normal lists are a sum type (AKA tagged union): they can either be empty (usually represented with the symbol `nil`), or they can be a pair containing a value and another list (usually represented as a function call `cons(myValue, myList)`).

Notice that the second possibility for normal lists corresponds exactly to our representation of non-empty lists. We can think of a list as being either empty or a non-empty list. Likewise we can think of a non-empty list as a pair of a value and a list.

Now this all seems quite recursive, self-referential and circular (which it is!), but that's just our mental model. When we actually write this down as a program we must be very explicit about what's going on. In particular, we cannot just throw pairs of things together and expect the compiler to figure out that these are lists/non-empty lists/etc.

> Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements?

No. You do that, manually, when you change the representation of your data. In particular, we must explicitly choose whether we're making a normal list or a non-empty list, and we must explicitly convert between the two as necessary (there is no magic!).

In Idris this might look something like:

    data List (t : Type) : Type where
      ListNil  : List t
      ListCons : t -> List t -> List t

    data NEList (t : Type) : Type where
      NECons : t -> List t -> NEList t

Now we can write functions which deal with a List or with a NEList, but not both, since that would be a type error e.g. "Expected 'List t', got 'NEList t'" (note that we can code to an interface, and there are some interfaces like `Mappable` or `HasLength` which can be implemented by both types, but that's another topic!).

> Does a zero-length list offer a different methods than a list that contains some elements?

Yes. If we have a non-empty list, we can get its first element (AKA the "head") and we can get a list of any following elements (AKA the "tail"):

    -- The head function is trivial for NEList
    neHead : (t : Type) -> NEList t -> t
    neHead t (NECons x ys) = x

    -- The tail function is trivial for NEList
    neTail : (t : Type) -> NEList t -> List t
    neTail t (NECons x ys) = ys

These functions are easy for NEList, but they only work for NEList; we can't pass these a List since that will be a type error. We also can't write a head or tail function for List, since there's no way to handle the Nil case:

    -- The head function is impossible to write for List, since there's no valid
    -- return value when we're given Nil
    lHead : (t : Type) -> List t -> t
    lHead t (ListCons x ys) = x
    lHead t ListNil         = {-WHAT COULD POSSIBLY GO HERE?-}

    lTail : (t : Type) -> List t -> List t
    lTail t (ListCons x ys) = ys
    lTail t ListNil         = {-WHAT MIGHT GO HERE?-}

The head function is impossible to write for List, since there's nothing which makes sense for Nil. For the `lTail` function we could actually return `Nil` and that would type check, but it's debatable whether that actually makes sense.

> Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements?

No. We do that when we "add elements" using either `ListCons` or `NECons`: if we use the `NECons` we get back an `NEList` which we can pass to functions like `neHead` and `neTail`. If we instead chose to use `ListCons` then we'd get back a normal List, which would give a type error if we tried to use it with `neHead` or `neTail`.

Notice that if we used a `ListCons` value, we know what the return values of `lHead` and `lTail` should be. Yet the compiler doesn't know that (it's not magic!), so it doesn't allow us to write such functions.

This is what we mean when we say phrases like "convincing the compiler that such-and-such", or that there are "proof obligations to fulfil": the thing we want to do might be perfectly reasonable (e.g. taking the `lHead` of a `ListCons` value) but the compiler forbids it because there appear to be unhandled cases (`ListNil`) and it's too dumb to figure out that they don't apply. The way we "convince" the compiler is to manually rearrange our data into a different form, where we can handle all of the possibilities (like `NEList` which only has the `NECons` case).

Notice that we can easily convert an `NEList` into a `List`, if we need to (e.g. to use a function which only works on `List`):

    -- Some function we might want to use, which we've only defined for List
    lLength : (t : Type) -> List t -> Int
    lLength t ListNil         = 0
    lLength t (ListCons x ys) = 1 + lLength ys

    -- It's easy to convert an NEList to a List, since NECons contains the arguments
    -- we need for ListCons
    neToL : (t : Type) -> NEList t -> List t
    neToL t (NECons x ys) = ListCons x ys

    -- We can get the length of an NEList by converting it to a List first
    neLength : (t : Type) -> NEList t -> Int
    neLength t ne = lLength (neToL ne)

What if we try to "trick" the compiler into taking the head of a List, by first converting a List into an NEList? It turns out to be impossible, precisely because there's no valid (type-correct) value we can use when we've been given ListNil:

    -- It's impossible to convert a List to an NEList, since there's nothing we can
    -- use as the first argument of NECons when we only have Nil
    lToNE : (t : Type) -> List t -> NEList t
    lToNE t (ListCons x ys) = NECons x ys
    lToNE t ListNil         = NECons {-WHAT COULD GO HERE?-} Nil

Notice that the first argument to NECons must have type `t`, but that could be anything since it's one of our arguments! The same goes for the return value of "head" above. Remember that Idris, etc. don't have a "null" value, so there's nothing we could put here (Haskell would let us use "bottom", i.e. a runtime error, but Idris prevents that unless we disable its totality checker).

As for going the other way ("eliminate the 'remove()' method"), notice that the second argument of NECons is a List, not an NEList. This means that when we remove an element from a non-empty list (e.g. using `neTail`, or just pattern-matching on an `NECons` value) we get back a List, which we cannot pass to functions which require a non-empty list.

Perhaps that List we get back does actually contain some elements. Yet the compiler doesn't know this (it's not magic!), and it certainly has no reason to think so. If we know that the tail of some NEList is actually non-empty, then we need to "convince the compiler" by converting it into an NEList. As we saw above, we cannot do that in general (since not all lists are non-empty!), but we might be able to do so on a case by case basis, i.e. by figuring out the correct value to pass as the first argument of NECons in each specific case.

You can think of a list as being either an empty list or a non-empty list, and think of those two possibilities as having different types. But it's unclear to me why that's any more reasonable than saying that an integer is either zero or a non-zero integer, and those two are different types.

And if you're going to say that zero and non-zero integers are the same type, I have one word for you: division.

And if you're going to say that it is in fact reasonable to divide integers this way, because in fact if you're doing division you do have to care about whether the denominator is zero, then... um... then you may in fact have a bit of a point.

To my thinking, though, tracking this through types at compile time is more work, and possibly also more error-prone, than tracking it by looking at the values at run time - certainly for the integer example, and maybe for the list example as well.

> it's unclear to me why that's any more reasonable than saying that an integer is either zero or a non-zero integer, and those two are different types.

Sure, that's actually very similar to the list case. We can think of natural numbers as being lists of unit/null values (since the only information we can get from such a list is its length; the elements are uninformative). This corresponds to the "peano numerals", sometimes referred to as unary. Imagine we take the definition of `List` above and get rid of the variable `t`, replacing all of its uses with `Null` (a single-element type containing only the value `null`). The first argument to `ListCons` will then have type `Null`, but since we know that's always going to be `null`, we can just drop that argument. Renaming things appropriately, the result is the following:

    data Nat : Type where
      Zero : Nat
      Succ : Nat -> Nat

We can clearly make this into a non-zero natural, in the same way we made non-empty lists: we just define a type that only has "Succ" (stands for "successor", i.e. one-more-than):

    data NZNat : Type where
      NZSucc : Nat -> NZNat

The only values of NZNat are successors of some Nat, and hence can't be zero.

We can represent integers in a few ways: one way is to use a pair of natural numbers, and treat their difference as the integer (e.g. `(10, 0)` is 10, `(0, 10)` is -10). Personally I prefer to use the following representation:

    data Int : Type where
      IZero     : Int
      IPositive : Nat -> Int
      INegative : Nat -> Int

`IZero` obviously represents zero, whilst `IPositive` and `INegative` take a natural and represent counting up or down by that amount + 1, i.e. `IPositive 9` is 10, `INegative 9` is -10.

Again, we can drop the `IZero` to get a non-zero integer:

    data NZInt : Type where
      NZPositive : Nat -> NZInt
      NZNegative : Nat -> NZInt

NOTE: It is not the case that we have some integer value, like `3`, and we're trying to think of the "best type" for it. That's putting the cart before the horse. Rather, we don't have any values until we define some types. Let's say we choose to write the above definition of `Int` in our program; after we do that, we can use it to define values like `IPositive (Succ (Succ Zero))`, which represents/behaves-like the integer `3`. Alternatively, we could choose to write down the `NZInt` definition, and use that to define values like `NZPositive (Succ (Succ Zero))` which is a different value, but also represents/behaves-like the integer `3`. We could also choose to write both implementations, in which case we can have multiple representations of numbers (similar to how we can represent numbers with `int`, `float`, `double`, etc. but some have problems).

In other words, we're not asking "given a number like 3, which type should we apply to it?", rather we're asking "which type of numbers should we pick", which depends more on our task than some 'platonic' property of the numbers themselves.

Also note that none of the examples I've given require dependent types at all; they could all be done in Haskell, StandardML, etc. (the list examples use generics AKA parametric polymorphism)

I actually wrote a blog post about these sorts of types (Nat, List, etc.), along with some that use dependent types like "lists of length N", "numbers less than N", "proof that N is less than M", "proof that X is an element of list L", etc. at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html

I also wrote a blog post based on another long-winded HN comment I made about dependent types ;) http://chriswarbo.net/blog/2017-11-03-dependent_function_typ...

> To my thinking, though, tracking this through types at compile time is more work

Oh absolutely! That's why it should be introduced only as needed. A language like Idris allows this stuff, but doesn't require it.

> and possibly also more error-prone, than tracking it by looking at the values at run time

I would say it causes more programmer errors, since there are conversions and stuff to keep track of, but almost all get caught by the compiler. If it's something that you actually want to check specifically then I think it's better to do at compile time; I wouldn't bother for stuff that could just be left for a catch-all exception handler in a main-loop or something.

I was mostly joking... I understand how dependent types work and don't think those researching it are of "ill repute."

It's worth pointing out though what is the real flaw with union types and dependent types: syntax might obscure it but the actual program is riddled with conditional logic and it is very hard to reason about such types in practice. People like to call this "pattern matching" but in reality such code, where each function is generally doing if (x instanceof Y) over a set, is exactly the sort of code that we try to avoid in modern systems.

All nontrivial programs are riddled with conditional logic. The difference is whether or not this conditional logic is exposed at the type level. Every single time you branch over anything in your code (say, to check if a list is empty before calling a function that will fail on an empty list), you could bubble that branch up to the type level in a full dependently-typed language, and have the compiler do that check for you. (Of course, this doesn't necessarily mean you'd always want to!)

Dependent types can be hard to work with because you have to hold the compiler's hand and tell it that yes, actually, the list you're working with at the point you want to call this function is definitely non-empty, and you can prove it by providing an instance of that type. So if you want to make a function that takes two non-empty lists l1 and l2 and spits back out a non-empty list l3 which is l1 ++ l2, in addition to the standard list append functionality, you need to show that l1 ++ l2 actually is non-empty.

But the fact that you have to do so much of this manually is, in my (professional) opinion, more a limitation of what we can currently automate than an inherent limitation of dependent types.

Sometimes you want the same guarantees, but it's easier to keep this separate from the list type. So you just write plain old vanilla list append, and then later on your inhabit the type that proves that for any two lists l1 and l2, l1 ++ l2 is non-empty. There are tradeoffs here: later on when you need a proof that (l1 ++ l2) is empty, you'll have to explicitly reference the type you found a term for earlier to show it to the compiler. If you put it into the list type itself, then you only need to do that once, when you write the append function. On the other hand, you also have to construct a whole bunch of other functions this way, and you might not actually care about the result being non-empty in those cases.

Also in my professional opinion, switching back and forth between these representations will be easier very soon. There are probably dozens of fantastic researchers all over the world working on making this easier, and we've made a lot of progress these past few years!

Regardless, deciding what you actually want to expose at the type level and how you want to expose it is an important design problem, and it depends a lot on what you want to be able to prove about your system without ever running your code.

> exactly the sort of code that we try to avoid in modern systems

What has "modern" got to do with any sort of value judgement? "Modern systems" could just as well be describing a tangle of Node.js spaghetti plugged into an unstructured pile of nosql data.

> each function is generally doing if (x instanceof Y) over a set

Your description sounds like some poor approximation of algebraic datatypes encoded in classes or something. I could imagine that being horrible. That doesn't mean that algebraic datatypes are horrible.

Personally, I found OOP to be very difficult to get my head around for the first few years; after that, I found it to mostly be used as an excuse for bloat, boilerplate and architecture astronautics (true story: I was once called "too academic" for using PHP's `array_map` function, by someone who thought it was perfectly reasonable to have a class called `ServiceControllerServiceProvider`...).

I find algebraic datatypes (sums/unions and products) to be much easier to reason about. In particular the data model is closed: these are the only possible cases we'll run into, handle them and we're done. OOP takes the other side of the "expression problem": its set of methods is closed, but we never know if some unexpected subclass might be passed in.

Also note that `instanceof` isn't particularly applicable in languages like Idris, Agda, Haskell, etc. since they're based on type theory, where typing is a judgement not a proposition (see e.g. https://ncatlab.org/nlab/show/judgment#in_type_theory ). Whilst in e.g. set theory we might query whether or not an element is in a set, e.g. using `x ∈ ℤ`, in these languages everything has a (principal) type, and saying something like `x : Int` is just asserting/defining/constraining that the value has that type. In particular it doesn't give us any information to branch on (it's either correct, and couldn't be otherwise; or it's incorrect, and the program won't compile). Also there are no subtypes, so if the type signature says we have a `Foo` then it's definitely a `Foo`. Personally, after using and encountering many type systems, I've never seen a version of subtyping that seemed 'worth it', i.e. where the extra expressiveness or guarantees outweighed all of the edge-cases, co-variant/contra-variant gotchas, etc. By the way there's a great explanation of why OOP and classes are a poor implementation of subtyping at http://okmij.org/ftp/Computation/Subtyping/

> syntax might obscure it but the actual program is riddled with conditional logic and it is very hard to reason about such types in practice

If you're actually in favour of class-based OOP, then surely you realise that exactly the same thing applies to dynamic dispatch of method calls?

The removeLast() function signature would be UntypedCollection (S n) -> UntypedCollection n

(S n) stands for successor of n. (Think of (S n) as n+1)

Given this, you can't call removeLast() on an UntypedCollection Z (empty collection) because the types wouldn't match.

So it's not by magic - the compiler knows the number of elements in the collection, because that value is part of the type. That's the entire point of dependent types - you get to have any value as part of a type.

The part that becomes tiresome very quickly - is convincing the type checker that what you want is valid. You have to provide proofs for the most trivial things (2+1 = 1+2) and the way it is currently achieved, is not programmer friendly.

Reply on news.ycombinator.com