Behavioural up/down casting for statically typed languages
summary
A typestate-based Java tool called JaTyC typestate checker attaches protocols to classes and now supports upcasts and downcasts in the middle of an object’s protocol by constructing union and intersection typestates and re-running a simulation-based subtyping algorithm where needed. The casting theory is mechanised casting theory with Coq proofs of soundness, implemented on the Checker Framework and open-sourced; practical tests show expressive handling of real Java patterns, though full type-safety relative to a core language is future work.
AI-written summary · about
chapters (13)
- 0:00Behavioural up/down casting intro
- 2:01Improving polymorphism in static typing
- 3:38Subtyping relations in protocols
- 5:29Downcasting with union types
- 6:57Upcasting with intersection types
- 8:04Type state in if branches
- 12:37Type state definitions
- 13:23Java Type State Checker
- 14:37Future work and tools
- 15:18Q&A
- 17:09Q&A: Explicit vs inferred states
- 19:14Q&A: Casting in OOP
- 20:05Q&A: Type state after casting
related talks
15mTaming Type Annotations in Gradual Typing
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
16mGradually Typing Strategies
19mA Dependently Typed Language with Dynamic Equality
46mThe Art of Java Type Patterns
26mType Narrowing the Hard Way
46mThe Calculated Typer (Functional Pearl)
40mDomain Specific Type Systems