caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Christopher Zimmermann <christopher@gmerlin.de>
To: caml-list@inria.fr
Subject: Re: [Caml-list] SOLVED: How to narrow polymorphic variant phantom types
Date: Thu, 17 Jan 2019 10:42:29 +0100	[thread overview]
Message-ID: <20190117104229.3afa7d13@mortimer.gmerlin.de> (raw)
In-Reply-To: <20190113084919.5cfaa055@mortimer.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 --]

      parent reply	other threads:[~2019-01-17  9:42 UTC|newest]

Thread overview: 3+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-01-13  7:49 [Caml-list] " Christopher Zimmermann
2019-01-13 10:10 ` Christophe Troestler
2019-01-17  9:42 ` Christopher Zimmermann [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20190117104229.3afa7d13@mortimer.gmerlin.de \
    --to=christopher@gmerlin.de \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).