RE: [Caml-list] Re: immutable strings (Re: Array 4 MB size limit)

["Harrison, John R" <johnh@ichips.intel.com>]

Hi Martin,

| OK, but let's be pragmatic: what kind of interface and implementation
do
| you have in mind?

I did indeed have a very specific example in mind, my theorem prover HOL
Light. I have an OCaml type of typed lambda-terms:

  type term =
      Var of string * hol_type
    | Const of string * hol_type
    | Comb of term * term
    | Abs of term * term

The type "term" is private, and the abstract type interface only permits
you to construct well-typed terms, via interface functions like "mk_var"
and "mk_comb". For example, the call "mk_comb(s,t)" gives "Comb(s,t)"
provided the types agree, and fails otherwise.

I would like the user to be able to write "mk_var(x,ty)" and the net
result to be just one cons "Var(x,ty)" with "x" and "ty" identical to
the
input arguments. But with mutable strings, it is possible in principle
for the string "x" inside that object to get modified by other code.
Of course, it's a bit artificial, but I would like it to be impossible,
given that the principle of LCF provers is that the user should be able
to use arbitrary programs while having soundness enforced by the ML
type system.

Of course, I can use my own private type of strings, but then I need
to convert every time I use standard library functions, pattern matching
is a bit less convenient, etc.

John.