- For Monday, January 26
- Read Ramsey, 2.1 - 2.3.
- Write a couple of paragraphs reflecting on what you find most difficult and most clear in these sections. The spirit here is that of dialogue with me and with others in the class. I am not looking for a "right answer" here, but rather an honest self-assessment of what you've learned from this first encounter with our material. What ideas make you want to know more? Were there concepts that remain inaccessible?
The 'build and learn by doing' is big for me as I often understand things better after I have worked through a few examples."
"I am having trouble understanding the big picture that the author is trying to communicate ... I am still uncertain what the Impcore language is used for and how it is used to build programming languages."
"ASTs provide a clear illustration of a programming language's structure ... I want to know more about how ASTs relate to the bigger picture."
"I am not sure if I understand how Impcore has three distinct environments."
- For Wednesday, January 28
- Read Ramsey, 2.4 (though we'll really dive into that material on Friday).
- Do any four of Problems 3–9 (you can certainly do more!), and also do Problem 10.
- I will send you the source code package for the Impcore interpreter by email. Please do not make this available on the wider internet.
- For Friday, January 30
- You should have completed reading through 2.6, though it's fine to skip 2.5 for now.
- Do any two of Problems 13, 15, 18, 20, and 21. It's fine if you want to work with a classmate on these.
"Operational semantics is a bit confusing, but I am guessing it is similar if not equivalent to interpreting the meaning of some outline of abstract syntax." [Close. It's more a way of explaining in a mathematically rigorous fashion what a correct interpreter for a program must do.]
- For Friday, February 20
- Complete reading of sections 3.1 - 3.11.
- Do Problems 2, 9, and 10, from Chapter 3.
- For Wednesday, April 1
- Read Section 6.1.
- Compare the type rules for Typed Impcore with the operational semantics from Chapter 2. Give your best explanation of the correspondence between type rules and operational semantics rules. This can be with a sentence or two, with a diagram, or some other mechanism of your devising (just pick something that you would use to explain it to someone else).
- For Wednesday, April 8
- Read Section 6.2 - 6.5.
- In Monday's class, we did a workshop on proof techniques for reasoning about a language's type system and operational semantics. We finished with a discussion of the challenges in formulating a theorem in a way that is amenable to formal proof—particularly with the technique of rule induction&mhash;and in relating of the inductive hypothesis (on subexpressions, or, equivalently, on expressions with smaller abstract syntax trees or shorter proof trees in the derivation of their types) to the theorem you're trying to prove.
- For Wednesday, April 8, you were asked to construct precise statements of the theorems in Problems 2–4 (Chapter 6), then construct versions of inductive hypotheses that are suitable for proving these theorems through rule induction.
- For Friday, April 17
- Read Section 6.6, at least through 6.6.3, and preferably all of it.
- On pages 257 and 258, Ramsey gives five rules for kinds. For each one, give an example from a real programming language (your choice, but not τμScheme), which corresponds to the concept the rule is expressing.
- For Wednesday, April 28
- Read Michael Schwartzbach, "Polymoprhic Type Inference", which available from the Readings page.
- In class yesterday, I showed informally the way that substitutions are calculated during the type inference process, in order to compute the principal type scheme of an expression.
- Here's an example in the spirit of yesterday's work:
- This is much more formal than anything we did yesterday, and you shouldn't focus too much on perceived technical details (several are missing). The important thing to grasp is the way that substitutions of type variables for types arise from the constraints discovered in the process of type-checking the expression (lines 3, 7, 8, 11, 13, 14, 16, and 20).
- In preparation for class tomorrow, I want you to think about this process on your own. Using one of the following examples, show the substitutions that arise in the derivation of the expression's type. This is all legal ML code, so you can check the types against your manual work. You don't have to get every constraint, and you don't have to get any particular evaluation order. The goal here is to build some intuition about the central task of Hindley-Milner type inference, namely the way that substitutions support the computation of an expression's principal type scheme.
- fun filter f nil = nil | filter f (x::xs) = if (f x ) then x::(filter f xs) else (filter f xs); Hint: think about what the type of the constant function if must be, based on your typechecking code above
- fun applyAll (nil,x) = nil | applyAll (f::fs, x) = (f x)::(applyAll(fs,x));
- fun fold_list ( f, nil, init) = init | fold_list (f, (x::xs), init) = f ( x, (fold_list (f, xs, init)));
- fun map_fold ( f, ls ) = fold_list ( (fn (x,v) => (f x)::v), ls, nil); Hint: if you don't get the same type as that of "regular" map(), something is wrong.
fun map f nil = nil | map f (x::xs) = (f x)::(map f xs); 1. map: a1 -> a2 -> d (defn., shortcutting a couple of substitution steps) 2. nil: a3 list (defn.) 3. d = a3 list (1,2) 4. x:a4 (var. intro) 5. xs:a5 (var. intro) 6. (::): a6 * (a6 list) -> (a6 list) (defn.) 7. a4 = a6 (4,6) 8. a5 = a6 list (5,6) 9. (x::xs): a6 list (6,4,5) 10. (x::xs):a2 (1,defn.) 11. a2 = a6 list (1,9,10) 12. f: a -> b (defn. -- "(f x)" makes this clear) 13. a1 = a -> b (1,12) 14. a = a4 (4,12, "(f x)") 15. (x::xs): a list (7,13) 16. a2 = a list (1,10,15) 17. (f x): b (4,11,defn. of function application) 18. ((f x)::(map f xs)): b list (16, defn.) 19. ((f x)::(map f xs)): d (defn.) 20. d = b list (17,18) 21. map:(a -> b) -> a list -> b list (1,12,15,20)