Coalton's type system is unsound in the presence of mutation

[eliaslfox]

Coalton currently uses a type system based on Hindley-Milner type classes added. This is unsound in the presence of mutation as shown by the following example.

(coalton-toplevel
  (define _
    (progn
      (let v = (make-vector))
      (vector-push 5 v)
      (vector-push "hello" v)
      (traceObject "vector" v)))) ;; vector: #.(VECTOR #<LISP-OBJECT #(5 "hello")>)

In Haskell mutation is only allowed in the IO monad making this a nonissue.

In coalton however mutable values can be defined in let expressions. In the above example the type of v is (Vector :a). This allows v to be used in both calls to vector push which are typed as (Integer -> (Vector Integer) -> Unit) and (String -> (Vector String) -> Unit) respectively. For the above code to be type safe the first call of vector-push must change the type of v to (Vector Integer).

A somewhat similar feature already exists in the language in the form of the monomorphism restriction. The following code does not type check.

(coalton-toplevel
  (define _
    (progn
      (let eql = ==)
      (eql 5 5)
      (eql "hello" "hello"))))

;; Failed to unify types STRING and INT
;; in unification of types (STRING → STRING → :A) and (INT → INT → BOOLEAN)
;; in definition of _
;; in COALTON-TOPLEVEL

When a definition of a variable in a let expression has non static predicates, then the variables in those predicates are resolved to their first usage. In the above example the type of eql is FORALL. :A -> :A -> Boolean, if it was defined as a function and thus not subject to the monomorphism restriction that its type would be FORALL A. :A -> :A -> Boolean.

The monomorphism restriction only looks at the types of bindings, however that would be insufficient to correctly type check the following example.

(coalton-toplevel
  (define _
    (progn
      (let v = (make-vector))
      (let f = (fn (x) (vector-push x v)))
      (let g = (fn (x) (vector-push x v)))
      (f 5)
      (g "hello")
       v)))

From this example it is clear that calling f must change the type of v to (Vector Integer). This type system feature exists in Ocaml and is documented here.

[eliaslfox]

See also Relaxing the Value Restriction

[eliaslfox]

See also weak type variables.