[comp.lang.functional] ML vs CL Type Systems

peterson-john@cs.yale.edu (John C. Peterson) (11/19/90)

Warning: I just implement these silly languages, not design them!

Wolfgang Grieskamp writes:
  >As i remember from a short afair with LISP some years ago, type 
  >declarations in CL are always monomorphic: no parametric 
  >polymorphy, no type variables. 

  >Hence the "far more generalicity" you mentioned is to omit types? 

It is hard for me to compare an essentially untyped language like CL
with a ML with regard to polymorphism.  CL supports polymorphic
functions as does ML (at least in the implementation sense).  The
implementation of cons is essentially the same in either language.
Where these two different styles diverge is in the inference process.
In CL, I can use a declaration like

(declare (ftype (function ((function (t) t) (list t)) (list t)) map))

while in Haskell (sorry - can't ever get ML syntax correct!)

map :: (a -> b) -> [a] -> [b]

(I'm taking liberties with the CL declaration; I don't believe `list'
has the correct predefined meaning, although it could).

What is interesting here is that where the ML declaration uses a type
variable, the CL declaration uses `t', sort of an anonymous type
variable.  In CL, the ability to connect the types of the different
arguments to map during inference is lost (although some CL guru will
probably point out a way to do it in CL).  This then leads to the
weakness in inference.  In Haskell, type inference can see 

map (+) [1,2,3]

and determine that the resulting list also contains integers; the CL
type system does not allow this based on the type signature of map.

The CL type system is more general in that is can describe types such
as `prime', which would be defined in procedural manner, or `even'.
What the CL type system does very well is subtyping; any subtype can
be described and many of these descriptions are completely
declarative.  Performing compile time inference is hard, but possible.
(Run time checking is trivial but slow).  CL inference techniques are
usually ad-hoc and cannot be applied to many of the types expressible.
The ML type system is much simpler and the inference process in
clearly defined but the types are not as expressive.

Without a precise definition of terms (which I have no intention of
providing), comparisons such as these usually degenerate into arguments
over the precise meaning of typing and related issues.  The whole
concept of type is approached from different directions in these two
languages, making many comparisons meaningless.  Things that I would
do with a type declaration in CL would require some sort of pragma
mechanism in ML; the compile time type security that ML provides is
unavailable in CL.

Thats enough rambling - this subject doesn't really merit this much of
my time anyway!

  John Peterson
  peterson-john@cs.yale.edu