3.17 Analysis: Type Systems

The suggested length is 5 pages.

Write a paper about type systems.

You can write about whatever you want provided you demonstrate a solid understanding. Here are a few suggestions you might consider in starting this assignment, but please do not feel constrained by this list, as it is not comprehensive. Please feel free to contact me directly so we can discuss the direction you want to take with the paper.

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