Question 1 @ 2024-12-03 18:28

What would the picky typechecker (extended with division) do with the following code:

(Assume the first version: the explicitly-typed one.)

---

• A It would only throw an error if the base language is eager
• B The typechecker’s role is only to erase the types, so it will do nothing
• C It won’t throw any type errors
• D It won’t throw any type errors, but that doesn’t avoid the runtime error
• E It will throw the obvious error due to the typo in the code

Question 2 @ 2024-12-03 18:30

When the third version of Picky (the ones without explicit type annotations and with ?T box types) is given the following:

it returns some long type error which can be simplified into:

What causes this error?

---

• A

  {fun {x} x} is the identity function — it is polymorphic, but our language doesn’t implement polymorphism.

• B

  Nothing is using the resulting value of the function call, which leaves the box uninitialized, leading to this error.

• C

  The problem is similar to our lazy evaluator: only when we want to show the value, we get to the requirement for a concrete type, leading to this error.

• D

  The toplevel requirement for all programs to evaluate to a NumT.

Question 3 @ 2024-12-03 18:36

What is the purpose of the “gamma” (Γ) in the Picky language’s typing judgments?

---

• A

  It keeps track of binding values during program execution.

• B

  It keeps track of identifier types during program execution.

• C

  It maps identifier names to their types during type checking.

• D

  It represents the set of all possible types in the language.

• E

  It holds the runtime stack of function calls.

• F

  It holds types during the “compilation” of typed to untyped code.

Question 4 @ 2024-12-03 18:38

Which of the following best describes a sound type system?

---

• A

  A type system that allows any program to compile, regardless of type errors.

• B

  A correctly-implemented type system that never crashes.

• C

  A type system that guarantees that well-typed programs do not produce runtime type errors when they terminate, with the specified value.

• D

  A type system that guarantees that well-typed programs do not produce runtime type errors provided they terminate with the specified value.

• E

  A type system where type checking occurs at runtime rather than compile time.

• F

  It doesn’t mean anything: all type systems are sound.