Re: [Caml-list] [Q]: Co(ntra)variance and subtyping?

[Didier Remy <remy@morgon.inria.fr>]

Alain Frisch <frisch@clipper.ens.fr> writes:

> > In the ML world, we mean complete type inference.
> 
> What does complete type inference mean ?  I would say that it implies
> that no type annotation is mandatory (if a program typechecks with a type
> annotation, it should also typecheck without). This property does not hold
> in OCaml; you can't remove type annotation in:
> 
> class o = object method f (x : int) = x end

Just to mention that examples can also be found in (almost) the core
language as well, you could choose ``ref []'' alone, which program will be
rejected by the compiler.

                              ----------------

I take this opportunity to raise a question about the meaning of "type
inference". Indeed, the answer of whether a language has type inference may
be more subtle than it first appears.  Checking whether types are/must be
mentioned in source programs may not be sufficient. Consider data-type
declarations:

        type 'a list = [] | Cons of 'a * 'a list 

Is this a type annotation?  Indeed, this declaration amounts to later
implicitly annotate every occurrence of a Cons as carrying arguments of
types 'a and 'a list.

The situation apparently looks simpler for the raw lambda-calculus, which
comes in two flavors untyped and typed and where the untyped version does
not mention types at all.  However, there is no untyped version of ML (with
datatypes/exceptions, etc.)  in the sense that types would not be mentioned
at all.

Even in the lambda-calculus it should be fair to consider that (fun x -> a)
carries the (implicit) type annotations ('a -> 'b).  So, isn't it unfair to
make a difference between type annotations that are plugged into the syntax
and more elaborated type annotations that would are explicitly in the
syntax. Formally, the distinction is not obvious: syntactic nodes (_ : t)
can well be seen as (i.e. replaced by) built-in primitives of types t -> t
(and given the same semantics as the identity).

Hopefully, there is always a lot of type information in programs, whether it
is implicit or explicit ---otherwise, type inference could not do much.
Furthermore, the difference between explicit and implicit annotations is not
always so clear, certainly not a binary notion.

My conclusions are that 

 - the typed and untyped version cannot be left implicit when talking about
type inference.

 - the property of ``having type inference'' should rather be replaced by a
measure of ``how much type inference'' (1) or ``what are the properties of
type inference'' (2). 

Answers to (2) the later can be made formal.  Answers to (1) tend to be
informal ---but it would be interesting to find a formal criteria...

        Didier Rémy
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr