A compilation method for dynamic typing in ML
summary
Presents a systematic compilation method that adds first-class dynamic typing to ML and ships in SML# 4.0.0. Uses type-directed compilation with type-tag passing and runtime generation of type tags, extends the framework with existential reification to handle locally bound type variables, and reifies ground values to user-level datatypes. Supports ML features intact: polymorphic type inference, user datatypes, pattern matching. Implements polymorphic pretty-printer, polymorphic JSON deserialization, type-safe DB interfaces and type-safe metaprogramming, and the implementation works.
AI-written summary · about
chapters (13)
- 0:00Motivations and the Goal
- 0:44Review of Dynamic Typing
- 1:22ML with orthogonal Dynamic Typing (overview) IV
- 3:25Contribution: Reification of Ground Types and Values
- 4:50Contribution: Record Compilation Method for Dynamic Typing
- 8:07The Source Calculus
- 8:38The Target Calculus II
- 9:15Operational Semantics and Type Soundness
- 10:04Type Soundness of Compilation
- 10:39Full Implementation in SML# Syntax and supporting structure Dynandc
- 11:48Example: Pretty Printing
- 12:36Example: JSON
- 13:42Example : Meta-programming II
related talks
21mPolymorphic Type Inference for Dynamic Languages
41mThe Dialectics of Type-Level Programming
24mUnfolding ML Datatype Declarations Without Loops
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
29mMsML: A Proposal for a successor ML
23mBetter Defunctionalization through Lambda Set Specialization
15mType-safe generation of modules in applicative and generative styles
30mDotty and types: the story so far