From: Goswin von Brederlow <goswin-v-b@web.de>
To: caml-list@inria.fr
Subject: Phantom types and polymorphic containers
Date: Fri, 05 Mar 2010 16:27:47 +0100 [thread overview]
Message-ID: <87pr3i94b0.fsf@frosties.localdomain> (raw)
Hi,
I'm wondering if one can create a polymorphic container with Phantom
types that can store types that themself have phantom types and get the
two to correlate. So far I've only been able to create a non-polymorphic
container with phantom types and even that isn't perfect:
Say I have my phantom typed string:
module S : sig
type 'a t = private string
val make : string -> [`Read | `Write] t
val make_const : string -> [`Const | `Read] t
val read_only : [> `Read] t -> [`Read] t
val get : [> `Read | `Const] t -> int -> char
val set : [> `Write] t -> int -> char -> unit
end = struct
type 'a t = string
let make x = x
let make_const x = String.copy x
let read_only x = x
let get x i = x.[i]
let set x i c = x.[i] <- c
end
And then my (non-polymorphic) Container:
module C : sig
type ('a, 'b) t = private 'a S.t ref
val make : 'a S.t -> ('a, [`Read | `Write]) t
val read_only : ('a, [> `Read]) t -> ('a, [`Read]) t
val get : ('a, [> `Read]) t -> 'a S.t
val set : ('a, [> `Write]) t -> 'a S.t -> unit
end = struct
type ('a, 'b) t = 'a S.t ref
let make x = ref x
let read_only x = x
let get x = !x
let set x y = x := y
end
Now to test this: (this is the expected behaviour)
# let s = S.make "write";;
val s : [ `Read | `Write ] S.t = "write"
# let c = C.make s;;
val c : [ `Read | `Write ] C.t = {contents = "write"}
# C.set c s;;
- : unit = ()
# let s2 = C.get c;;
val s2 : [ `Read | `Write ] S.t = "write"
# S.set s2 0 'C';;
- : unit = ()
# let d = C.read_only c;;
val d : ([ `Read | `Write ], [ `Read ]) C.t = {contents = "write"}
# C.set d s;;
^
Error: This expression has type ([ `Read | `Write ], [ `Read ]) C.t
but an expression was expected of type
([ `Read | `Write ], [> `Write ]) C.t
The first variant type does not allow tag(s) `Write
# let s2 = C.get d;;
val s2 : [ `Read | `Write ] S.t = "write"
# S.set s2 0 'W';;
- : unit = ()
# let s = S.read_only (S.make "read");;
val s : [ `Read ] S.t = "read"
# let c = C.make s;;
val c : [ `Read ] C.t = {contents = "read"}
# C.set c s;;
- : unit = ()
# let s2 = C.get c;;
val s2 : [ `Read ] S.t = "read"
# S.set s2 0 'C';;
^^
Error: This expression has type [ `Read ] S.t
but an expression was expected of type [> `Write ] S.t
The first variant type does not allow tag(s) `Write
But one thing doesn't quite work:
# let s1 = S.make "foo";;
val s1 : [ `Read | `Write ] S.t = "foo"
# let s2 = S.read_only s1;;
val s2 : [ `Read ] S.t = "foo"
# let c = C.make s2;;
val c : ([ `Read ], [ `Read | `Write ]) C.t = {contents = "foo"}
# C.set c s1;;
^^
Error: This expression has type [ `Read | `Write ] S.t
but an expression was expected of type [ `Read ] S.t
The second variant type does not allow tag(s) `Write
I would like c to accept [> `Read] strings. I want a signature like this:
val set : ('a, [> `Write]) t -> [> 'a] S.t -> unit
and I think the get would have to change then to:
val get : ('a, [> `Read]) t -> [> 'a] S.t
But [> type] only seems to work with specific polymorphic variant types
and not with polymorphic types:
# type 'a foo = [`A | `B];;
type 'a foo = [ `A | `B ]
# type ('a, 'b) f = ([> 'b] as 'a) -> unit;;
^^
Error: The type 'a is not a polymorphic variant type
# type ('a, 'b) f = ([> 'b foo] as 'a) -> unit;;
type ('a, 'b) f = 'a -> unit constraint 'a = [> 'b foo ]
At least I can't find how.
Any ideas how to make the container polymorphic?
MfG
Goswin
reply other threads:[~2010-03-05 15:29 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
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=87pr3i94b0.fsf@frosties.localdomain \
--to=goswin-v-b@web.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).