Fine-grained types with more general library

Fine-grained types with more general library

[Dawid Toton]

I have a type (e.g. of path to file)

type path = string list

 and many operations (e.g. path manipulation). Then I need to have two 
kinds of paths (e.g. local and remote) and want type system to enforce 
proper usage (some functions act on remote paths only etc.). So I create 
new two types:

type remote_t = Remote path
type local_t = Local path

Then I avoid using type path for greater safety. But I have a problem: 
can't use path manipulation library on these new types. I have created 
"mirror" versions of the library for each new type, but this made my 
source code unmaintainable. What is the right solution?

I'd prefer not to contaminate the path library with things specific to 
this particular problem, since it's reused.

Dawid

Re: [Caml-list] Fine-grained types with more general library

[Edgar Friendly]

Dawid Toton wrote:
> I have a type (e.g. of path to file)
> 
> type path = string list
> 
> and many operations (e.g. path manipulation). Then I need to have two
> kinds of paths (e.g. local and remote) and want type system to enforce
> proper usage (some functions act on remote paths only etc.). So I create
> new two types:
> 
> type remote_t = Remote path
> type local_t = Local path
> 
> Then I avoid using type path for greater safety. But I have a problem:
> can't use path manipulation library on these new types. I have created
> "mirror" versions of the library for each new type, but this made my
> source code unmaintainable. What is the right solution?
> 
> I'd prefer not to contaminate the path library with things specific to
> this particular problem, since it's reused.
> 
> Dawid
> 
type 'a path = string list
type remote_t = `Remote path
type local_t = `Local path

val works_on_remote_t : [> `Remote] path -> whatever
val works_on_local_t : [> `Local] path -> whatever
val works_on_any_t : 'a path -> whatever

See the following URL for more details on this trick (called Phantom Types):
http://caml.inria.fr/pub/ml-archives/caml-list/2001/09/081c77179ee2a3787233902a51633122.en.html

E

Re: [Caml-list] Fine-grained types with more general library

[Bünzli Daniel]

Le 10 févr. 08 à 20:15, Edgar Friendly a écrit :

> type 'a path = string list
> type remote_t = `Remote path
> type local_t = `Local path

Yes, but make sure that the type path is abstract or private otherwise  
it won't work.

Daniel

Re: [Caml-list] Fine-grained types with more general library

[Dawid Toton]

> type 'a path = string list
> type remote_t = `Remote path
> type local_t = `Local path
>
> val works_on_remote_t : [> `Remote] path -> whatever
> val works_on_local_t : [> `Local] path -> whatever
> val works_on_any_t : 'a path -> whatever
>
> See the following URL for more details on this trick (called Phantom Types):
> http://caml.inria.fr/pub/ml-archives/caml-list/2001/09/081c77179ee2a3787233902a51633122.en.html
>
>   
Thank you all for immediate responses!
After playing with toplevel I managed to get the correct syntax:

type 'a path = string list
type remote_t = [`Remote] path
type local_t = [`Local] path

This seems as yet to be very good solution.:)

Dawid

Re: [Caml-list] Fine-grained types with more general library

[David Teller]

I'm not sure I understand the question. Still, if you haven't used
phantom types yet, it sounds like the right thing to do:
 type 'a path = string list
 type remote_t = Remote path
 type local_t  = Local path

Now, you can write things such as

val print_local : Local path  -> unit  (*only works on local paths*)
val print_remote: Remote path -> unit  (*only works on remote paths*)
val print_any   : 'a path     -> unit  (*works with either*)

Does this help you ?

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.