What is Soft Typing?

:: HOPL

By: Ben Greenman

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

Important details:

  • 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?

If you:

  • 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.

Clarification

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

Types t are made of constructors k, flags 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 | ....

where:

  • U is just a symbol, represents “union”
  • a is a type variable; there are infinitely many type variables
  • b is 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 k is 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