Re: [Caml-list] Coinductive semantics

[Andrej Bauer <Andrej.Bauer@andrej.com>]

skaller wrote:
> basically I don't know enough theory to turn the purely
> algebraic finite array types -- fairly useless in practice --
> into variable length arrays required in practice.
> [By variable I mean the length is an immutable dynamic type,
> not that you can change the length of the array]

If I understand you correctly, you have types [0], [1], [2], [3], ...,
one for each natural number 0, 1, 2, ... (to avoid confusion I want to
distinguish notationally between number n and type [n] here, even if
Felix does not do it). Let me call [n] "the type of indices of arrays of
length n". We may think of [n] as the set {0,1,2,...,n-1}.

You know how to deal with the type [n]->t, which is an array of length n
containing t's. Now you would like to "make n variable (dynamic)". This
sounds like a dependent type to me, i.e, you want not just a bunch of
types [0], [1], [2], ... but rather a _type constructor_ [-], which maps
from int to types. You may define it in dependent type theory (I am
going to use set-theretic notation so that I don't confuse everyone):

  [n] = {k : int | 0 <= k and k < n}

In set theory, this is interpreted as follows: an index of an array of
length n is an integer k. This integer must be between 0 and n.

In type theory, this is interpreted as follows: an index of an array of
length n is a _pair_ (k,p) where k is an integer and p is a proof of the
fact k is between 0 and n.

The type of arrays you're talking about is a dependent sum

  't array = sum (n:int) [n]->'t

An element of this type (according to type theory) consists of a pair
(n,a) where n is an integer and a is a map [n]->'t, i.e., an array of
length n. Elements of such an array are indexed by pairs (k,p).

If everyone believed in type theory, compilers would be easy to write.
Every time a programmer wanted to address an element of an array, he
would provide not just the index k but also the proof p that k is a
valid index. Compiler would just have to check that p is a valid proof
(easy when p is a formal proof). But programmers don't want to do that.

If we care about soundness and safety, we are left with two
possibilities: either the compiler or the run-time environment must
supply the missing proof p. For the run-time environment this is easy,
because k and n are always instantiated to particular constants and we
may simply check that 0<=k<n. But for the compiler, it is an impossible
task, since k and n may be arbitrarily complex expressions. The compiler
would have to be able to solve undecidable problems in order to
determine whether an index is valid. You're hitting the theoretical
limit of static type checking.

There may be special cases where compiler can determine whether the
index is ok. For example, if the index is a linear function of a bunch
of integer variables, which is typical of array computations as long as
you're _not_ simulating a matrix as a one-dimensional table or some
such, then you're in the realm of Presburger arithmetic (integers, +, -,
<, =, and multiplication by _constants_ only) which has a decision
procedure (double exponential time, if I remember it right). I am sure
people have looked into this sort of thing. Good luck!

Andrej