Re: [Caml-list] fighting the type system

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

On 2011/03/24, at 7:01, Joel Reymont wrote:

> How do I do this?
> 
> 	Thanks in advance, Joel

Well, you don't because this is clearly unsound.

> --- Util.ml
> 
> type 'a writable = < write : Protocol.t -> unit; .. > as 'a
> 
> module type Endpoint = 
> sig 
>  val request : unit -> 'a writable
>  val response : 'a writable -> 'b writable
>  val read_request : Protocol.t -> 'a writable
>  val read_response : Protocol.t -> 'a writable
> end

Your definition of 'a writable is actually equivalent to writing

  class type writable = object method write : Protocol.t -> unit end

and replacing uses of 'a writable by #writable.
The trouble is that returning a value of type #writable is unsound,
since it means that this value has any possible method, including write.
So you would be able to write:
     (request ())#foo
and have the type checker happily comply.

I'm not sure of what you're trying to do.
If you just want the Endpoint interface to specify an object type
containing at least write, you could use a private row type:

module type Endpoint = 
sig
 type writable = private <write : Protocol.t -> unit; .. >
 val request : unit -> writable
 val response : writable -> writable
 val read_request : Protocol.t -> writable
 val read_response : Protocol.t -> writable
end

You can then instantiate it with a concrete type, using
   Endpoint with type writable := mywriter

Jacques Garrigue