Gradual Typing

Reference 1

RUST ——–buffer——–> Ocaml <———————

Escape Hatches:

ML:C FFI Rust:unsafe Java: JNI

All type soundness(safety) guarranttes are gone.

Instead, use Principled FFIs:

  • ML: linear types.

Linking types: support safe initeroperability with other languages.

  • Only need linking types extensions to interact with behavior/features inexpressible in your language.
  • SNAPL’172: Linking Types for Multi-language Software: Have your cake eat it too.
  • Teach Ocaml with ownership in Rust:
    • Linking Type: linear type: cannot keep it and give it away at the same time. Ownership in Rust.

Pure vs Stateful languages

Semantic Foundations for Gradual Typing

Slow migration from dynamic typing to static typing.

Mixed with dynamic & static types. EG: C#, Typescript, Hack, Flow, Dart.

Cast Calculus: cast dynamic type to static type.

What is Semantics of Casts?: What a cast should be checking or not checking is the heart of where the research area is. Three main questions:

  • Gradual Typing Criteria: How do you set up the semantics of casts.
  • Frameworks for Gradualizing: AGT framework
  • Performance Overhead. (sound gradual typing dead? )

relational reasoning. soundness.

Criteria

  • Gradual: precision: make the types more precise; change to more precise: either error or behave the same.
  • Soundness:
    • Milner: “Well typed programs cannot go wrong”
    • Equational Reasoning Priciples
  1. FM 2019, PPDP Invited Talk: Semantic Foundations for Gradual Typing.video ↩
  2. SNAPL’17: Linking Types for Multi-language Software: Have your cake eat it too. ↩
Created Oct 9, 2019 // Last Updated Oct 9, 2019

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?