[Haskell-cafe] Solved but strange error in type inference
oleg at okmij.org
oleg at okmij.org
Wed Jan 4 14:48:14 CET 2012
One should keep in mind the distinction between schematic variables
(which participate in unification) and universally quantified
variables. Let's look at the forall-elimination rule
G |- e : forall a. A
-------------------- E
G |- e : A[a := t]
If the term e has the type forall a. A, we can use the term at some
specific type t. Often the type checker doesn't know which specific
type t to choose. Therefore, the type checker inserts a schematic type
variable X (think of Prolog logic variable), to defer the
decision. Further down the type-checking road, more information
becomes available and it will become clear what concrete type t to
use. Like in Prolog, a logic variable denotes a guess, or a promise,
to be forced later (there is a deep connection between laziness and
logic variables). So, the forall-elimination rule becomes
G |- e : forall a. A
-------------------- E
G |- e : A[a := X]
Let's look at the forall-introduction rule
G |- e : A [a := aeigen]
-------------------- I where aeigen \not\in G
G |- e : forall a. A
To type-check that a term e has a polymorphic type (which happens when
the user gave a type signatures which contains type variables,
implicitly quantified), the type-checker generates a fresh, unique
_constant_ (called eigenvariable) and type-checks the term with the
constant substituted for the type variable. If the term type-checks,
it does have the polymorphic type.
(One may ask why this fresh constant is called eigen_variable_ if it
doesn't actually vary. That is a very good question, answered in
http://okmij.org/ftp/formalizations/inductive-definitions.html#eigenvariables
).
GHC calls these eigenvariable rigid variables.
The upshot: eigenvariabes are constants and can't be changed by
unification. Schematic variables are variables and can be substituted
by unification. Quantified type variables are replaced by schematic
variables when _using_ a polymorphic term. Quantified type variables
are replaced by constants (or, rigid variables) when _type-checking_ a
term.
The earlier example:
f :: a -> a
f x = x :: a
can be alpha-converted [recall, ScopedTypeVariable extension is off] as
f :: a -> a
f x = x :: b
First the type-checker generates beigen.
To check if 'f' can indeed be given the type signature a -> a,
GHC generates the eigenvariable aeigen and type-checks
(\x::aeigen -> x :: beigen) :: aeigen
The problem becomes obvious. The error message is very precise,
describing the precise location where type variables are bound.
Couldn't match type `a' with `b'
`a' is a rigid type variable bound by
the type signature for f :: a -> a at /tmp/e.hs:2:1
`b' is a rigid type variable bound by
an expression type signature: b at /tmp/e.hs:2:7
In the expression: x :: b
In an equation for `f': f x = x :: b
Again, read `rigid type variable' as eigen-variable.
In OCaml, type variables are schematic variables (in many
contexts). For example:
# let f1 (x:'a) = (x:'b);;
val f1 : 'a -> 'a = <fun>
# let f2 (x:'a) = x + 1;;
val f2 : int -> int = <fun>
The function f2 is not polymorphic at all, although it may appear so
from the use of the type variable 'a.
But in other contexts OCaml does work like GHC:
# module F : sig val f5 : 'a -> 'a end = struct
let f5 x = x + 1
end;;
Error: Signature mismatch:
Modules do not match:
sig val f5 : int -> int end
is not included in
sig val f5 : 'a -> 'a end
Values do not match:
val f5 : int -> int
is not included in
val f5 : 'a -> 'a
Further, OCaml has now a specific construct to introduce rigid type
variables (which appear as type constants).
# let f4 (type a) (x:a) = (x:a) + 1;;
Characters 25-26:
let f4 (type a) (x:a) = (x:a) + 1;;
^
Error: This expression has type a but an expression was expected of type int
More information about the Haskell-Cafe
mailing list