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

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

[Christopher Zimmermann]

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


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 --]

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

[Christophe Troestler]

On 13 January 2019 at 08:49 CET, Christopher Zimmermann wrote:
>
> […] 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.

How about

    val dup : ([< `Read | `Write ] as 'a) perm -> 'a desc -> 'a desc

?

Cheers,
C.

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

[Christopher Zimmermann]

[-- 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 --]