Coinductive semantics
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Andrej Bauer <Andrej.Bauer@a...> 
Subject:  Re: [Camllist] Coinductive semantics 
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,...,n1}. 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 settheretic 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 runtime environment must supply the missing proof p. For the runtime 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 onedimensional 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