Types Considered Harmful (Benjamin C Pierce)

[bearophile]

Andrei:

> http://www.reddit.com/r/programming/comments/ftgok/types_considered_harmful/

It's an interesting slides pack, but it's not easy to follow for me, it assumes some knowledge I don't have yet.

>From the slides:

>Fancy types make the programmer's head hurt<

Languages are used to solve many different problems. In different problems you want different static constaints. Pluggable type systems are a partial solution to that problem. If your problem is simple, you don't plug a fancy type system, and you avoid some migraines. If your problem is hard, you create a tailored type system that's good for the problem.


>Is it better for Jane Programmer to write ~20 more or less correct lines of code / day or ~0 perfect ones?

If Jane has to create a little web site with a limited purpose that may be OK, expecially if someone else later fixes the code or if Jane later adds more tests to cach most bugs. If the software system to be created is control software for a oil rig, or worse for a X-ray scanner for people, then 0 perfect ones is better.


>Why is Hindley-Milner such a sweet spot?<

It has some disadvantages too, Scala has not adopted it.


>Precise types reveal too much. Precise types can force details of issues like resource usage into interfaces<

I don't know/understand what the author is talking about.


>cf. Morrisett's story about region types in Cyclone...<

Maybe this is the paper "Analysis issues for cyclone", by Morrisett, but it's not avilable for free.


P.26: >More research is needed! :)<

The smile is present because they are researchers, so more research means some more paid work.


>Computing is full of situations where we want to compute some function, edit the output, and "push the edits back" through the function to obtain a correspondingly edited input.<

I'd like to read a list of examples, because I don't know many similar situations.
I have found a paper named "Quotient Lenses" that list some situations:

>Most programs compute in a single direction, from input to output. But it is often useful to take a modified output and "compute backwards" to obtain a correspondingly modified input. For example, if we have a transformation mapping from a simple XML database format describing classical composers to comma-separated lines of ASCII we may want to be able to edit the ASCII output (e.g., to correct the erroneous death date above) and push the change back into the original XML. The need for such bidirectional transformations arises in many diverse areas of computing, including data synchronizers (Foster et al. 2007a,b), parsers and pretty printers (Fisher and Gruber 2005; Eger 2005), marshallers and unmarshallers (Ramsey 2003; Kennedy 2004), structure editors (Hu et al. 2004), graphical user interfaces (Meertens 1998; Evers et al. 2006; Greenberg and Krishnamurthi 2007), software model transformations (Stevens 2007; Xiong et al. 2007), system configuration management (Lutterkort 2007), schema evolution (Miller et al. 2001; Cunha et al.; Berdaguer et al. 2007), and databases (Bancilhon and Spyratos 1981; Dayal and Bernstein 1982; Bohannon et al. 2006, etc.).<

I don't understand several of the things shown in the last pages. But I think D contracts don't assign blame correctly. This means that in a program like this, the (assert) error is shown at line 3, instead of at the calling point, at line 6, where it's meant to be (like with template constraints):


void foo(int x)
    in {
        assert(x >= 0); // line 3
    } body {}
void main() {
    foo(-1); // line 6
}


When the stack trace will be present (on Windows) this situation will improve.

Bye,
bearophile