Lectures onType Theory
ch:subtyping: ch:subtyping
appendix sectiontutorials

ch:subtyping: ch:subtyping

Exercise 18.16.

Read the corpus’s Ty, context, and decision datatypes before the algorithm. Trace a variable query to its source bound, an arrow query through contravariant/covariant premises, and a universal query through one fresh binder. Run the four standard Kappa commands on artifacts/ch18-subtyping/corpus.kp; require seven PASS lines, the final count, and an empty audit. Then replay separately the README’s arrow-variance, promotion, and freshening mutations. Each mutant must remain well typed and must fail the inline stdout oracle. Do not reinterpret the fuelled Full-F<: root as a total decision procedure.

Search the book

Type to search the local edition.