Question 1 @ 2024-04-16 18:09
When Picky3 (the one without explicit type annotations and with the ?T
box types) is used with the following program:
{call f {< 1 2}}}
it refuses to run and throws a verbose type error that boils down to something like:
got `BoolT -> BoolT`
What causes this error?
-
{fun {x} x}is the identity function — it is polymorphic, but our language doesn’t implement polymorphism. -
Nothing is using the resulting value of the function call, which leaves the box uninitialized, leading to this error.
-
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.
-
It is caused by the toplevel requirement for all programs to evaluate to a
NumT.
Question 2 @ 2024-04-16 18:12
A language with a sound type system…
-
Is much improved with good speakers.
-
Allows you to easily add new types.
-
Guarantees completeness.
-
Guarantees no infinite loops.
-
Guarantees runtime types using a static analysis.
-
Guarantees static types from a dynamic analysis.
-
Guarantees no runtime errors will ever happen.
Question 3 @ 2024-04-16 18:14
Alice wants to add typechecking to a language where + can work with
any two values via coercion. She takes the Picky language (assume
Picky2, though it doesn’t matter), and adds coercion from any kind of
value to a number when needed. Then, she adds the following two
judgments instead of the single one:
———————————————————— ————————————————————
Γ ⊢ {+ A B} : Number Γ ⊢ {+ A B} : Number
Bob notes that there is a major flaw in this suggestion. What is it?
- Some values cannot be coerced to a number.
- Coercion implies subtypes, which we cannot do in an HM typesystem.
- Coercion implies an OOP language, which we don’t have.
- It is unsound, since we typecheck only one side.
- It is eager, which contradicts coersion.
Question 4 @ 2024-04-16 21:21
The underlying theme of continuations is fundamentally about:
-
Laziness vs Eagerness
-
Control flow
-
Static types
-
Infinite loops
-
Compilation techniques
Question 5 @ 2024-04-16 21:23
What can we say about the CPS process?
-
It needs to be done selectively: locally in places that require IO or other side-effects.
-
It needs to be done globally, CPS-ing a function forces all its callers to be CPS-ed as well.
-
It needs to be guided by IO types similar to the Slug types.
-
It requires the original code to be functional code: no IO, mutations, or other side-effects.