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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: David Teller <David.Teller@univ-orleans.fr>

>  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?

I'm not sure how far you can go with this approach, but if all you
want is to know the type inferred for witness, while this type is
clearly not generalizable (otherwise you won't be able to collect
information), I can think of several tricks.

* first remark: ocamlc -i works even with non-generalizable types, as
  it does not generate any .cmi.

* if you want to be still able to compile, you can write a .mli file
  not including the witness. ocamlc -i on the .ml will still show you
  the witness.

* other solution: put everything inside a function, so that the
  type variable is still generalizable after typing the function.

Hope this helps,

Jacques Garrigue