A soft type system rewrites programs and meets a few design criteria.
What are the Design Criteria?
According to Mike Fagan’s 1991 dissertation, a soft type system must:
- accept all syntactically correct programs as input;
- produce equivalent, memory-safe programs as output; and
- be unobtrusive
- In this context, memory safe basically means “no segfaults”. Programs output by a soft type system should be as safe as statically-typed Java programs or dynamically-typed Python programs.
- Fagan characterizes unobtrusive with two general principles:
- minimal text principle : the type checker should work without any programmer-supplied annotations
- minimal failure principle : the type checker should assign useful types to idiomatic programs (basically, don’t just say that every expression has “unknown” or “top” type)
Why would I want to use a soft type system?
- like dynamic typing
- want some benefits of static typing
- refuse to (or cannot!) change your code to satisfy a type checker
then Soft Typing is a perfect fit. You just need to find/build a soft type checker.
The benefits of static typing that a soft type system can give are:
- early detection of typos and simple logical errors
- documentation, through (inferred) type signatures
- speed, when the types can justify removing a runtime safety check
See Andrew Wright’s 1994 dissertation for proof.
Can I use Andrew Wright’s soft type system?
Not sure, but you may download the code for it:
Please explain Fagan’s / Wright’s soft types
t are made of constructors
f, and type variables
a. The grammar for types is basically:
t ::= a | (k f t ...) U t k ::= Int | Pair | -> f ::= ++ | -- | b a ::= a0 | a1 | a2 | a3 | .... b ::= b0 | b1 | b2 | b3 | ....
Uis just a symbol, represents “union”
ais a type variable; there are infinitely many type variables
bis a flag variable; the set of flag variables is also infinte
There are also some rules for types to be well-formed.
Here are two well-formed types:
(Int ++) U a0 (-> ++ ((Int b0) U a1) ((Int ++) U a2)) U a3
Here are two types that match the grammar, but are NOT well-formed:
(Int ++ a0) U a1 (-> --) U a2
Finally, some intuition:
- A constructor
kis like a behavior,
- a type describes the behaviors a value can have.
- The description is like a bitvector of “yes”, “no”, or “maybe” for each possible behavior.
- A flag variable is the way to say “maybe”.
- Every type ends with a type variable because every typed expression might flow to a context that expects a more general type.
The type and flag variables let Fagan and Wright encode subtyping using polymorphism. It’s a very cool idea, introduced in Didier Remy’s POPL 1989 paper. But it adds a learning curve, and has some drawbacks for type inference.
Stream-of-consciousness notes from the HOPL lecture