Question 1 @ 2025-04-15 19:00

When we extended our Picky language with a recursive binder, the type judgment that we used was:

The difference from the previous plain binder (with) is the use of an extended Γ:

How does this enable recursion?

---

• A It ensures that V typechecks with a function type
• B It allows V to conatin a free occurrences of x
• C It checks that τ₁ is a valid type
• D It guarentees that evaluating V will halt

Question 2 @ 2025-04-15 19:05

What properties of a typechecker did we discuss?

---

• A Composability
• B Completeness
• C Openness
• D Extensibility
• E Soundness

Question 3 @ 2025-04-15 19:07

Of the two relevant typechecking properties, completenes and soundness, which one is more important?

---

• C1 Completeness is more important, since it makes it possible to write any code.
• C2 Completeness is more important, since it allows us to avoid infinite loops.
• S1 Soundness is more important, since it means that the typechecker is correct.
• S2 Soundness is more important, since it ensures that the typechecker implementation is itself typechecked.

Question 4 @ 2025-04-15 19:09

What is the main difference between the type system of Typed Racket (TR) and of Picky?

---

• A TR is less advanced in that it cannot do full type inference.
• B TR is strongly normalizing.
• C TR is a Hindley-Milner type system.
• D TR allows arbitrary type unions, not just disjoint ones.
• E TR types are proper sets.

Question 5 @ 2025-04-15 19:10

Which of the following statements are true about a Hindley-Milner type system?

---

• A All types are a subtype of a “top” type.
• B Most types can be inferred.
• C All toplevel types must be declared rather than inferred.
• D Subtypes and supertypes can be created using unions and intersections.
• E It is strongly normalizing.
• F It is the underlying type system in Typed Racket (and TypeScript).