Re: [Caml-list] SOLVED: How to narrow polymorphic variant phantom types

[Christopher Zimmermann <christopher@gmerlin.de>]

[-- Attachment #1: Type: text/plain, Size: 2531 bytes --]

It's contravariance (type -'a desc) I was looking for.
This is how it can be typed:

module Io : sig
  type 'a perm  constraint 'a = [< `Read | `Write ]
  val ro : [ `Read ] perm
  val rw : [ `Read | `Write ] perm

  type -'a desc constraint 'a = [< `Read | `Write ]

  val open_file : 'a perm -> string -> 'a desc
  val dup : ([< `Read | `Write ] as 'a) perm -> 'a desc -> 'a desc
  val read : [> `Read ] desc -> string
  val write : [> `Read | `Write ] desc -> string -> unit
end

On Sun, 13 Jan 2019 08:49:19 +0100
Christopher Zimmermann <christopher@gmerlin.de> wrote:

> In the following simplified program I'm trying to use phantom
> types to express read / write / read_write permissions.
> This program fails at runtime in the call to Io.write.
> Is it possible to adjust the phantom types so that it fails at
> compilation time?
> I'd like to express a typing like
> val dup : 'a perm -> [< `Read | `Write > 'a] desc -> 'a desc
> but a type variable inside the polymorphic variant type is not
> allowed.
> 
> module Io : sig
>   type 'a perm  constraint 'a = [< `Read | `Write ]
>   val ro : [ `Read ] perm
>   val rw : [ `Read | `Write ] perm
> 
>   type 'a desc constraint 'a = [< `Read | `Write ]
> 
>   val open_file : 'a perm -> string -> 'a desc
>   val dup : 'a perm -> [< `Read | `Write] desc -> 'a desc
>   val read : [> `Read ] desc -> string
>   val write : [> `Read | `Write ] desc -> string -> unit
> end
> = struct
>   type 'a perm = [ `Ro | `Rw ] constraint 'a = [< `Read | `Write ]
>   type 'a desc = Unix.file_descr constraint 'a = [< `Read | `Write ]
>   let ro : [ `Read ] perm = `Ro
>   let rw : [ `Read | `Write ] perm = `Rw
> 
>   let open_file perm file =
>     Unix.(openfile
>             file
>             [match perm with |`Ro -> O_RDONLY |`Rw -> O_RDWR]
>             0o000
>          )
>   let read desc =
>     let buf = Bytes.create 10 in
>     assert (Unix.read desc buf 0 10 = 10);
>     Bytes.unsafe_to_string buf
>   let write desc buf =
>     let buf = Bytes.unsafe_of_string buf in
>     assert (Unix.write desc buf 0 (Bytes.length buf) = Bytes.length
> buf)
> 
>   let dup desc = Unix.dup ?cloexec:None
> end
> 
> let () =
>   let fd_ro = Io.(open_file ro "/tmp/test") in
>   let fd_rw = Io.(dup rw fd_ro) in
>   Io.write fd_rw "Hello, World";
>   print_endline (Io.read fd_ro);
> 
> 



-- 
http://gmerlin.de
OpenPGP: http://gmerlin.de/christopher.pub
CB07 DA40 B0B6 571D 35E2  0DEF 87E2 92A7 13E5 DEE1

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 833 bytes --]