What is Soft Typing?

2017-04-28 :: 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:

https://github.com/nuprl/softscheme

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.

Inside PRL