Type-indexed Data
•
Benefits
–
The type system disallows ill-formed Terms like:
–
(If (Int 3) (Int 0) (Int 9))
–
Documentation
•
Problems
–
How do we type pattern matching?
–
case x of
–
(Int n) -> . . .
–
(Bool b)-> . . .
–
What type is x?
•