1. 17

proof that your program will terminate

Or that a coprogram will be productive (services/servers/streaming fall under this).

Most programs these days operate on codata, so termination on a per-destructed-codata-component basis is productivity if I understand correctly.

(ejenk touches on this in the comments as well, but I wanted to add this point)

  1.  

  2. 3

    Okay, out of curiosity, could someone implement the:

    float myDivide3(float a, float b, proof(b != 0) p) {
        return a / b;
    }
    

    function given in the article?

    1. 5

      Well, here’s the code in Agda. If you know a little FP it shouldn’t be too terrible.

      I reimplemented just about everything except numbers for “learning purposes”. In practice this could be shortened by using the stdlib much more heavily, in particular we can hack out the divisions of Eq, not, False, ProofPair and so on and so on.

      Update: Here’s the version with the stdlib.

    2. 1

      A little note on the first comment:

      not just a la halting problem, but wouldn’t the proof be a 3SAT problem on the order of (# of inputs) * (number of operations prior to the call to divide), making it pretty much intractable?

      You can work around this by not allowing programs that you can’t prove terminate.

      Edit: and of course, I should have read the responses better but that is what people say in the thread as well.

      1. 1

        I think dependant types are a bit like an of explict formulation of many of results static analysis tools provide via data propagation. Essentially they provide different fixes to the same problem - that sometimes you want to constrain Values to avoid error conditions, not just types. I’ve not yet been persuaded that making these constraints explicit via Dependant Types is really worth the added typing and complexity. I like that static analysis tools can be used to solve lots of these issues without me having to do anything. Personally I am more interested in the development of Kinds. If you promote all constant Values and Types to Kinds you can solve some of the problems dependant types can be used for, but you also open up a bunch of cool meta-programming things also.

        1. 4

          The “without me having to do anything” part will never be possible since you quickly get into undecidability of constraints. On the other hand, dependent types are constantly requiring less from programmers, which is really awesome - we’ll just never be able to reach the point of having some magical complete inference.

          Dependent types develop kinds to be just functions at the type level. There’s no distinction, just a hierarchy, where the type of a value is Set0 and the type of that is Set1 and the type of that is Set2, and so forth, to avoid Russel’s paradox.

          And dependent types are really brilliant at meta-programming! See the metaprogramming in Agda repository from Conor McBride or just read the Idris tutorial for lots of examples.

          1. 3

            DT languages eliminate the distinction of kinds by creating and infinite hierarchy of types. Unless I’m mistaken about what you’re referring to.

            1. 2

              Interesting, I feel rather the opposite. Every time I’ve used a static analysis tool it’s felt like an ad-hoc, informally-specified implementation of half a type system. (And the times when a static analysis tool can figure something out without you having to do anything correspond exactly to the times when a type system can infer a type without you having to do anything, no?)

              (Kinds meanwhile are, thus far, too abstract for me to get any use out of, and I find the notation very confusing)