Version française
Home     About     Download     Resources     Contact us    
Browse thread
Polymorphic variant as a witness?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: David Teller <David.Teller@u...>
Subject: Re: [Caml-list] Polymorphic variant as a witness?

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.