Browse thread
Polymorphic variant as a witness?
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2008-06-23 (08:10) |
From: | Romain Bardou <Romain.Bardou@l...> |
Subject: | Re: [Caml-list] Polymorphic variant as a witness? |
Hello, Maybe I don't understand entirely your problem but it seems to me that this does what you want: # let x = ref `A;; val x : _[> `A ] ref = {contents = `A} # match !x with `B -> 1 | _ -> 2;; - : int = 2 # x;; - : _[> `A | `B ] ref = {contents = `A} # match !x with `C -> 1 | _ -> 2;; - : int = 2 # x;; - : _[> `A | `B | `C ] ref = {contents = `A} The type of x is expanded with more and more "effects" in a modular fashion (thanks to the _ pattern). In fact you do NOT want to generalize here, as generalizing would allow you to instantiate the type, whereas what you want is some kind of side-effect in the type, as far as I can understand. Did this help or did I miss something? :) -- Romain Bardou David Teller a écrit : > Dear list, > > I have been thinking for some time about using polymorphic variants to > encode some aspects of a types-and-effects type system in OCaml using > Camlp4. While the idea is still quite fuzzy, I have the feeling that, if > I could have a value (let's call it "witness") with type > [> ] ref > which I could "touch" into becoming > [> `A] ref > then > [> `A | `B] ref > etc. as effects `A, `B, etc. appear in the program, it could provide > interesting information on the effects of the program. > > Now, of course, I can't define a value with type ref [> ] or even with > type ref [> `dummy]. That is, when compiling a module consisting only in > a declaration such as > let witness = ref `dummy > I'm faced with the good old "cannot be generalised" error message. This > strikes me as normal -- I'm sure that, with the right modifications on > witness, I could cause runtime type inconsistencies for any client > attempting to read the value of witness. However, in this case, I'm not > going to read any value from witness, ever. I only want to "touch" it > into becoming something a tad more complex, which I could then look at > with ocamlc -i or such. > > My question is: is there a way to hijack polymorphic variants into doing > what I wish? Or to encode this behaviour somehow? > > Thanks, > David >