From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <oleg@okmij.org>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 2E6AA7EE49
	for <caml-list@sympa.inria.fr>; Tue, 17 Sep 2013 10:13:30 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  oleg@okmij.org) identity=pra; client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org";
  x-conformance=sidf_compatible
Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of
  oleg@okmij.org designates 66.39.3.115 as permitted sender)
  identity=mailfrom; client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@www1.g3.pair.com) identity=helo;
  client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org";
  x-sender="postmaster@www1.g3.pair.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AtUGACsOOFJCJwNzXWdsb2JhbABbFoMpwWeBNQMYBw4GPoIlAQEDAQF5BRY0VRQUDod0Bgy6SI9nBxaECAOXegGVGDw
X-IPAS-Result: AtUGACsOOFJCJwNzXWdsb2JhbABbFoMpwWeBNQMYBw4GPoIlAQEDAQF5BRY0VRQUDod0Bgy6SI9nBxaECAOXegGVGDw
X-IronPort-AV: E=Sophos;i="4.90,921,1371074400"; 
   d="scan'208";a="33168658"
Received: from www1.g3.pair.com ([66.39.3.115])
  by mail2-smtp-roc.national.inria.fr with SMTP; 17 Sep 2013 10:13:28 +0200
Received: (qmail 69328 invoked by uid 9370); 17 Sep 2013 08:13:27 -0000
Date: 17 Sep 2013 08:13:27 -0000
Message-ID: <20130917081327.69327.qmail@www1.g3.pair.com>
From: oleg@okmij.org
To: martindemello@gmail.com
CC: caml-list@inria.fr
In-reply-to:
	<CAFrFfuGg3n4m5AU1QtE6GahMgdfADfP6ohbrxd5zpM8ju-g97w@mail.gmail.com>
Subject: Re: [Caml-list] "subclassing" a char map


> 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.