Re: [Caml-list] Immutable strings

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2014/07/05 20:24, Gerd Stolpmann wrote:
> 
> Am Freitag, den 04.07.2014, 17:01 -0400 schrieb Markus Mottl:
>> I agree that the new concept has some noteworthy downsides as
>> demonstrated in the Lexing-example.  Your proposed solution 2
>> (stringlike) would probably solve these issues from a safety point of
>> view.  The downside is that the complexity of string-handling would
>> increase even more, because then we would have three types to deal
>> with.  I personally prefer safety over convenience, but other people's
>> (especially beginner's) mileage may vary.
> 
> Well, the complexity can be reduced a bit by using phantom types:
> 
> type string = [`String] stringlike
> type bytes = [`Bytes] stringlike
> 
> and then just define function-by-function what is permitted:
> 
> val get : 'a stringlike -> int -> char
> val set : [`Bytes] stringlike -> int -> char -> unit
> val sub : 'a stringlike -> int -> int -> [`String] stringlike
> val sub_bytes : 'a stringlike -> int -> int -> [`Bytes] stringlike
> 
> etc., and the modules String and Bytes would just contain aliases of
> these functions with monomorphed typing.
> 
> I don't know, though, whether we can be safe to never see the
> polymorphic typing when just using string and bytes. It would be a bit
> surprising for beginners to see that, and you sometimes would have to
> deal with unresolved type variables.

Indeed. Originally the plan was to use the above scheme for strings,
and use polymorphism to allow more flexibility. However, this is not
100% compatible, even if we allow to ignore the parameters, because
of these unresolved type variables. This also becomes complicated
when you want to take functions as parameters.

The stringlike type itself is a good idea.
In the standard library, it could be implemented as:
   type string = private stringlike
   type bytes = private stringlike
However, it is only about allowing passing string and bytes arguments
to functions in an homogeneous way.
For the return case, the situation is more confused, because returning
a stringlike is actually weaker than either bytes or string.
Alain’s idea of using an extra type-only parameter (‘a is_a_type) works,
and it doesn’t really need to be a GADT.
But this is a bit strange to use an extra parameter where a phantom type
on string itself would solve the problem. I.e., using your above approach
one can be safe just writing:
  val copy : ‘a stringlike -> ‘b stringlike
  val sub : ‘a stringlike -> int -> int -> ‘b stringlike
(assuming that we are always copying in sub too)

One could try to mix the two approaches: i.e. have a type ‘a stringlike,
with explicit coercions to and from bytes and string.
Note that you can do that yourself: create your own Stringlike module,
with the coercions
   type ’a stringlike
   external from_string : string -> [> `String] stringlike = “%identity"
   external to_string : [`String] stringlike -> string = “%identity”
   …
Note that you should not write “type +’a stringlike”, since you want to exploit
the fact any stringlike must be monomorphic.
This could of course be added to the standard library, but for compatibility
reasons I think that string itself has to stay as an abstract (or private) type with
no parameter. And the above kind of coercions is compiled away, so if your
goal is performance this should not be a problem.

Jacques