Notes on Idris (2017) (thebreakfastpost.com)

> 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?

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.

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

[–] drdeca 8y ago ↗