Re: [Caml-list] Polymorphic variant as a witness?

[Romain Bardou <Romain.Bardou@lri.fr>]

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
>