Hacker News Reader

Your "I-can't-work-with-this-unsized-list-because-I-need-to-pass-it-to-something-that-takes-a-sized-list" problem seems like something that one might _think_ would be a problem if one understood advanced types on a conceptual or theoretical level but not how to use them in real-world code. It's actually pretty easy to deal with cases like this... At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case where it doesn't. For example, you could pass the unsized list to a function which performs validation of its actual runtime size, returning, e.g., an `Option[List[Int] @@ MinSize[_5]]` (if I may use Scala-speak). You'd then have to handle both the case where the `Option` is a `Some` and the case where it's a `None`. Ultimately, it ends up being extremely similar to checked exceptions: you are simply forced to write code to handle all cases, rather than writing code that allows some of them to blow up at runtime (while telling yourself "that case could never happen in the real world" or "that's an edge case, we'll just ignore it").

> At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case where it doesn't.

I don't follow. If your list is not the right size, your program doesn't compile, period.

If it does, you're not using a dependently typed language.

Am I missing something?

I think you are. I think you are missing the possibility to write a total function of type `List[Int] => Option[List[Int]] @@ MinSize[_5]` (I'm still writing Scala-ish types because that's where I feel comfortable). This gets you into a world where you can deal with your previously-unsized `List` as a sized `List` (either you can map over your `Option` or you can fold the `Some` and `None` cases together by providing some default).

It depends on the language. For instance in Scala you can simulate collections of fixed size as in https://github.com/milessabin/shapeless/blob/master/core/src...

Then, at runtime, you can cast an unsized list to a sized list giving - say - a function List[A] => Option[Sized[List[A], N5]] that will fail if the list is not of size 5. From then on you can go on letting the compiler keep track of lengths.

Of course, this does not work at all if you have no clue what size your input will have

I believe that you don't need to know what size your input will have. Rather, you need to know what size the thing you will be calling will need, right?

Yes, you're missing this, I think: When you call a function which takes, say, a list-5, all you need to do is to prove to the compiler that you've checked that the list is indeed of length 5 before you pass it along.

The key insight here is that the check may be performed at compile time or runtime as long as the compiler can see that you've performed the check. It can do this e.g. in pattern match clauses. For example in code like

        case inputList of
           [a,b,c,d,e] -> branch-A
           otherwise   -> branch-B

Idris will automatically have proof that inputList is length 5 in branch-A. Which means you'd be free to call any function which expects list-of-length-5 in branch-A without further ceremony. This will not be the case for branch-B.

(And if you think about it... if you didn't allow for runtime checks to satisfy such proof obligations there would essentially no way for any dependently programs to depend on any runtime values at all.)

Aside: Another thing which I think has been missed in this entire discussion is that you don't have to actually use List-of-size-N as your type. If you don't actually care about the size of the list in the code you're writing, you're also allowed to just use List-of-any-finite-size as your data type. (Of course this could cause a certain amount of friction if the standard library is all based on List-of-size-N, but it shouldn't be too bad in e.g. Idris.)

I wish we (both potential users, and developers of these languages) would start seeing these things more like enhanced tests than perfect manifestations of mathematical truth.

Nobody would ever question the value of a unit-testing framework because it requires you to instantiate objects and doesn't hit the database and the ORM. (Yes, there are testing strategies that cover all of that, but for unit-testing application logic, you generally want to skip all of that.) Dependent types should let you do the same thing that a test would do, except exhaustively: if you add a new email address to an account with N addresses, you can then index N+1 of those addresses, but no more. The N-address account coming from the ORM isn't considered an "escape hatch" that "weakens the test system": it's just how it works.

I want stronger types for exhaustive testing of business logic on individual functions -- the sort of things that a comment would say (e.g. "Returns a subset of this parameter if it is provided, otherwise..."), except machine-checked. I don't need my entire program to have a type that Messrs. Curry and Howard like. In all probability, my entire program is structured as an infinite loop anyway.

I don't know that any systems really let you get here (other than maybe extraction of particular functions into Haskell or ML, but really the people who would voluntarily write their entire app in Haskell or ML are not the right target audience).

> How the hell does this work?

It's easy, since it works as it always did. You check whether the list coming from the database has the correct size n, and then the type system knows that and lets you pass said list to a function that expects a list of size n.

    list = GetAListFromTheDatabase()
    if(list.size == n){
       // type checker knows that the size is n here
       foo(list);
    }else{
       error("Database returned a list of incorrect size.");
    }

In a dependently typed language, an if statement isn't just a run-time check, it also provides a compile-time proof that its condition is true in one branch and false in the other branch. So your insinuation that run-time checks are not possible in dependently typed languages is false; you just have to prove at compile-time that all possible results of the run-time check have a valid execution path. So if you have an unsized array A, you can't just write `return A[5]`, but you can write `if (A.length() > 5) { return A[5]; } else { return 0; }`.

You're misguided. What you describe is not really an issue for dependent types. Your attitude seems to be shared by a lot of people, so I'll try to clear things up a bit. I think it helps if I use refinement types (as used in F), which are just dependent types in disguise.

Taking your example, I would have written a function f* that takes a list (with an arbitrary type of elements) and produces an integer. Its basic ML type would be:

  f : list 'a -> int

Now taking your example, assume that, for whichever reason, f only works for lists of length 5. This would probably never arise in practice, but I'm just going with your example. First, we have to say what "works" means. Intuitively, it means that f produces a reasonable output. Let's say we have defined a function p which says whether the output is reasonable. In F, I can state all of that by giving my function f* the type:

  f : l:list 'a{length l = 5} -> x:int{p x = True}

I can only give this type if I can convince the compiler that the result really satisfies p - this is one point I'll get back to later.

Now assume I want to use this function later in my code to deal with some user provided input. Assume I have a function read_int_list:

  read_int_list : () -> list int

I can now combine this function with f, but only if I ensure that the length of the read list is 5:

  val process_input =
    let inp = read_inst_list ();
    let res = if length inp = 5
                then f inp
                else -1  // error

This will now be accepted by the compiler, since it will be able to deduce that inp is an admissible input to f, because the function call was guarded by the if condition (I'll also get back to this). Note that the code above is absolutely no different than what you would write in any "regular" programming language (including ML). What is different is that in a regular language you could forget to add the condition - but not in F. Of course, the error handling code above is not sensible.

So interacting with user input and output is absolutely NOT a problem for dependently typed languages and their ilk. In fact, there is a full-blown implementation of the TLS protocol in F.

What is a problem, however, are the two points I hinted at: convincing the compiler that your statements are true. This is done in one of the two ways. First, you can manually give "hints" to the compiler, which is normally very tedious. Second, the compiler can try proving them automatically (F* for example leverages an SMT solver), which is great when it works, but often doesn't work.

So the real problem is that producing proofs is quite time consuming, and thus expensive. The world, as you put it, is not completely wrong: very often, a buggy program is cheaper than a correct one. Heck, people still stick to OpenSSL over the above verified TLS implementation - and for good reasons. The exceptions being programs used in NASA rovers and such - which is where you're starting to see dependent types being used. I certainly won't use them for my projects - at least not until the systems get massively better at producing proofs. It's partly happened with the advent of the SMT solvers, but it's nowhere near enough.

That's one of the reasons Pascal failed.