3.18 Analysis: Type Systems

In about 5 pages (approximately 325 80-character lines or 2,750 words), write a paper about type systems.

Provided you write intelligently and demonstrate your understanding of type systems you can write about whatever you’d like. If that is too vague for you, or if you need some guidance, here are some suggestions:

- Discuss why so-called "dynamically typed languages", like Python, Ruby, and Racket can be thought of as statically typed. (Feel free to read Bob Harper’s blog on this topic, but don’t drink his Kool-Aid too much. He’s making a curious reductionary argument that doesn’t correspond to how the concept of "dynamic typing" is generally understand. It’s really a very clever rhetorical argument in favour of static type systems.)

- Discuss the trade-off between safety and convenience in programming as related to type systems.

- Learn about the Curry-Howard isomorphism. Relate and discuss it.

- Discuss how you can encode invariants about data into your types, other than based simply on atomic types.

- How could you use types to guarantee that a piece of code does not modify the filesystem? Feel free to discuss what types you would give to the code, the filesystem accessors, etc.

- Discuss how type systems relate to laziness. Does laziness make a type system different? How?

- Discuss why type systems are conservative, as opposed to exact or liberal.

- Discuss why the simply-typed lambda calculus is strongly normalizing. Is that a good thing? In what situations?

- Read Functional Programming in C++, by John Carmack. How does this relate to this class and type systems.

- Discuss the difference between the Haskell and ML type systems. In particular, look into monads, type classes, and functors.

- Explain how type inference is related to Gaussian elimination and linear optimization.

- Discuss how type inference leads to "interesting" error messages. Can you think of ways to avoid this problem?

- Learn about the history of the so-called "value restriction" in ML. Relate and analyze it.

- Discuss the "occurs check" during type inference unification.

Refer to Language Analysis the First for details about including citations, history, code, etc in your writing in this class.