Polymorphic variant as a witness?

Polymorphic variant as a witness?

[David Teller]

      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

-- 
David Teller
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations. 

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

[Christophe TROESTLER]

On Sun, 22 Jun 2008 01:11:59 +0200, David Teller wrote:
> 
> I could have a value (let's call it "witness") with type 
>   [> ] ref

Why do you want it to be mutable?

> which I could "touch" into becoming 
>   [> `A] ref

Are you expecting to write [touch `A witness] so [witness] becomes of
type [[> `A] ref]?  If you can do with an immutable [witness], then
you can write a macro to that effet (use: [let witness' = TOUCH `A
witness]).  What exactly is your purpose?

Regards,
C.

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

[David Teller]

On Sun, 2008-06-22 at 01:27 +0200, Christophe TROESTLER wrote:
> On Sun, 22 Jun 2008 01:11:59 +0200, David Teller wrote:
> > 
> > I could have a value (let's call it "witness") with type 
> >   [> ] ref
> 
> Why do you want it to be mutable?

Because I know how to change the type of a reference to a polymorphic
variant (the touching) -- but not the type of an immutable polymorphic
variant.

> > which I could "touch" into becoming 
> >   [> `A] ref
> 
> Are you expecting to write [touch `A witness] so [witness] becomes of
> type [[> `A] ref]?  If you can do with an immutable [witness], then
> you can write a macro to that effet (use: [let witness' = TOUCH `A
> witness]).  What exactly is your purpose?

Say you are developing a Camlp4-based DSL in which
* file access may only be performed by some construction -- let's call
it FILE
* network access may only be performed by some construction -- let's
call it NET.

I'd like to take advantage of OCaml's type system to tell me if file
access and/or network access have taken place. Now, since I'm
implementing FILE and NET from within Camlp4, I can give them whichever
semantics I want. For instance, FILE could mean [touch `File witness;
foo] and NET could mean [touch `Net witness; bar]. If I write a program
containing FILE, OCaml's type system will have inferred that the type of
[witness] is [[> `File]]. Which would be great for me.

Now I know I could do that with monads. I could also implement a type
system for the DSL. I'm just wondering if polymorphic variants could
provide an alternative. Because if they can, it may have direct
applications to exception management for OCaml.


> Regards,
> C.

Cheers,
 David

-- 
David Teller
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations. 

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

[Romain Bardou]

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
> 

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

[Jacques Garrigue]

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

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

[David Teller]

On Mon, 2008-06-23 at 19:27 +0900, Jacques Garrigue wrote:
> From: David Teller <David.Teller@univ-orleans.fr>
> * first remark: ocamlc -i works even with non-generalizable types, as
>   it does not generate any .cmi.

Interesting. I'm not sure it's usable in my case, but it's interesting.

> * 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.

Also a good idea. Also possibly unusable in my case, but I'll need to
think about it further.

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

In that case, the witness remains invisible, doesn't it?

Thanks,
 David


-- 
David Teller
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations. 

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

[Jacques Garrigue]

> > * other solution: put everything inside a function, so that the
> >   type variable is still generalizable after typing the function.
> 
> In that case, the witness remains invisible, doesn't it?

No, the idea is to give the witness as argument to the function, so
that its type is inferred and generalized.
Of course this means that no side effects will occur until the
function is called, so the semantics is preserved.
And this way you can combine several such functions later by passing
the same witness to all of them.

Something like:

let touch (x:[> ] as 'a) (y:'a) = () 

let m1 w =
  let rec f1 ... = ... touch `A w ...
  and f2 ... = ... touch `B w ...
  in
  let r1 = ...
  and r2 = ...
  in
  (f1, f2, r1, f2)

let m2 w (f1, f2, r1, r2) =
  let rec f3 ... = ...
  in 
  let r3 = ...
  in
  (f3, r3)

let m1_then_m2 w = m2 w (m1 w)

These modules encoded as functions are combined in something close to
monadic style, but inside them you can just use your trick with
"touch w", with no need to sequence the witness. By the way, since w
is a function argument, it doesn't need to be of type "[> ..] ref"
here.

Note that the above approach is not going to be very precise.
If you share directly w, then m1 will have type [> `A | `B] -> ...
independently of whether f1 and f2 are actually used.
If you want to be more precise, you must parameterize functions with
witnesses.

let m1 w =
  let rec f1 w ... = ... touch `A w ...
  and f2 w ... = ... touch `B w ...
  in
  ...

This way you get a bit more control on when to merge effects.
Thanks to let polymorphism, it looks like you just get the same power
as with an effect system (you're still limited a bit by the value
restriction).

Also, you may have realized that the above code just uses functions to
do that same thing as functors. Functors would be syntactically nicer,
but they wouldn't let you infer the type of w, which is the whole
point. If getting data out of tuples proves to be a pain, you could
also return an immediate object.

Cheers,

Jacques Garrigue

Re: Polymorphic variant + phantom type as a witness

[Gleb Alexeyev]

I've been pondering about something along these lines (if I understand 
it correctly, it seems to resemble what Jacques Garrigue proposed - 
passing a witness as extra argument to every effectful function).

I didn't think it through and haven't use it in practice, so I don't 
know whether it's usable, but anyway:

module type Permission = sig
   type 'a t
end

module Permission : Permission = struct
   type 'a t = unit
   (* here we need some means to cook new permissions - this is the part 
I didn't think through *)
end

module type SafeEffect = sig
   (* signatures of effectful primitives to be used instead of functions 
from Pervasives *)
   val print : [> `IO] Permission.t -> string -> unit
   val setref : [> `State] Permission.t -> 'a ref -> 'a -> unit
end

module SafeEffect : SafeEffect = struct
   (* implementation ignores the witness *)
   let print _ s = print_endline s
   let setref _ r x = r := x
end

module Example = struct
   module S = SafeEffect

   let use_io effect () = (S.print effect "bar"; 42)

   let global_n = ref 0

   let use_state effect () =
     S.setref effect global_n 42

   let use_both effect () =
     use_io effect ();
     use_state effect ()
end


The inferred signatures expose the effects:
     val use_io : [> `IO ] Permission.t -> unit -> int
     val use_state : [> `State ] Permission.t -> unit -> unit
     val use_both : [> `IO | `State ] Permission.t -> unit -> unit