Re: [Caml-list] "subclassing" a char map

[oleg@okmij.org]

> I just wanted a type of char map I couldn't insert anything else other
> than A-Z into, that the typechecker would prevent me from mixing with
> the regular char map.

Using the abstract type and restricting its constructors -- that is,
controlling the ways the values of that type can be created -- lets us
statically ensure quite strong invariants. For example, subranging (as
in your A-Z example) or primality of integers, etc. The best part:
this type safety can be achieved without any dependent or other fancy
types, using any type system that supports abstract types.

That deep insight is from the 70s, and explained with great clarity in the
paper
        Protection in Programming Languages
        James H. Morris Jr.
        http://www.erights.org/history/morris73.pdf

His running example was also interval type. Incidentally, James
H. Morris has discovered quite a few other things we now take for
granted, for example, lazy evaluation
        http://www.cs.cmu.edu/~jhm/short%20biography.htm

The same insight -- the use of an abstract data type whose values can only
be produced by a trusted kernel, and the use of a type system to guarantee this
last property -- underlies Robin Milner's Edinburgh LCF theorem prover,
written at about the same time in early 1970s. ML was designed as a
scripting language of that prover.