English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
RE: [Caml-list] Re: immutable strings (Re: Array 4 MB size limit)
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-05-29 (20:52)
From: Harrison, John R <johnh@i...>
Subject: RE: [Caml-list] Re: immutable strings (Re: Array 4 MB size limit)
Hi Martin,

| OK, but let's be pragmatic: what kind of interface and implementation
| 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
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.