caml-list - the Caml user's mailing list
 help / Atom feed
* [Caml-list] How to narrow polymorphic variant phantom types
@ 2019-01-13  7:49 Christopher Zimmermann
  2019-01-13 10:10 ` Christophe Troestler
  2019-01-17  9:42 ` [Caml-list] SOLVED: " Christopher Zimmermann
  0 siblings, 2 replies; 3+ messages in thread
From: Christopher Zimmermann @ 2019-01-13  7:49 UTC (permalink / raw)
  To: caml-list

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

^ permalink raw reply	[flat|nested] 3+ messages in thread

* Re: [Caml-list] How to narrow polymorphic variant phantom types
  2019-01-13  7:49 [Caml-list] How to narrow polymorphic variant phantom types Christopher Zimmermann
@ 2019-01-13 10:10 ` Christophe Troestler
  2019-01-17  9:42 ` [Caml-list] SOLVED: " Christopher Zimmermann
  1 sibling, 0 replies; 3+ messages in thread
From: Christophe Troestler @ 2019-01-13 10:10 UTC (permalink / raw)
  To: Christopher Zimmermann; +Cc: caml-list


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.

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list https://inbox.ocaml.org/caml-list
Forum: https://discuss.ocaml.org/
Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 3+ messages in thread

* Re: [Caml-list] SOLVED: How to narrow polymorphic variant phantom types
  2019-01-13  7:49 [Caml-list] How to narrow polymorphic variant phantom types Christopher Zimmermann
  2019-01-13 10:10 ` Christophe Troestler
@ 2019-01-17  9:42 ` " Christopher Zimmermann
  1 sibling, 0 replies; 3+ messages in thread
From: Christopher Zimmermann @ 2019-01-17  9:42 UTC (permalink / raw)
  To: caml-list

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

^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, back to index

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-01-13  7:49 [Caml-list] How to narrow polymorphic variant phantom types Christopher Zimmermann
2019-01-13 10:10 ` Christophe Troestler
2019-01-17  9:42 ` [Caml-list] SOLVED: " Christopher Zimmermann

caml-list - the Caml user's mailing list

Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list

AGPL code for this site: git clone https://public-inbox.org/ public-inbox