[Caml-list] polymorphic variants question

[Caml-list] polymorphic variants question

[John Max Skaller]

Is there any way to avoid repeating a list of variants like:

type abcd = ['A | 'B | 'C | 'D];;
type abcde = [#abcd | 'E];;

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au 
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
New generation programming language Felix  http://felix.sourceforge.net
Literate Programming tool Interscript     
http://Interscript.sourceforge.net
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Polymorphic variants question

[David Allsopp]

Forgive the potentially obvious question --- I'm not very familiar with
polymorphic variants but I think that they're what I want in this situation!

Suppose I'm dealing with three constructors `A, `B and `C and I have a
function f that's supposed to take either `A or `C and return any of `A, `B
or `C. If I write:

let f x = if x = `A then (true, `B) else (false, x)

then I get the type

val f : ([> `A | `B] as 'a) -> bool * 'a

Now, if I try to constrain it to what I'm after with

let (f : [`A | `C] -> bool * [`A | `B | `C]) = fun x -> ...

then I get a type error unless I change
	(false, x)
to
	(false, id x)
with 
	let id = function `A -> `A | `C -> `C

Is there a better way of writing this? I'm using this in the context of
several interrelated lexers where `A, `B and `C are high-level states and
certain lexers can only be called in a subset of those states but each lexer
may yield any value for the next-state. I'd quite like to eliminate the id x
bit since it's only there to "separate" x from the return value for the
type-checker.

Thanks!


David

Re: [Caml-list] Polymorphic variants question

[Olivier Andrieu]

 David Allsopp [Friday 1 September 2006] :
 >
 > Forgive the potentially obvious question --- I'm not very familiar with
 > polymorphic variants but I think that they're what I want in this situation!
 > 
 > Suppose I'm dealing with three constructors `A, `B and `C and I have a
 > function f that's supposed to take either `A or `C and return any of `A, `B
 > or `C. If I write:
 > 
 > let f x = if x = `A then (true, `B) else (false, x)
 > 
 > then I get the type
 > 
 > val f : ([> `A | `B] as 'a) -> bool * 'a
 > 
 > Now, if I try to constrain it to what I'm after with
 > 
 > let (f : [`A | `C] -> bool * [`A | `B | `C]) = fun x -> ...
 > 
 > then I get a type error unless I change
 > 	(false, x)
 > to
 > 	(false, id x)
 > with 
 > 	let id = function `A -> `A | `C -> `C
 > 
 > Is there a better way of writing this? I'm using this in the context of
 > several interrelated lexers where `A, `B and `C are high-level states and
 > certain lexers can only be called in a subset of those states but each lexer
 > may yield any value for the next-state. I'd quite like to eliminate the id x
 > bit since it's only there to "separate" x from the return value for the
 > type-checker.

you can use pattern-matching with a "as" pattern to introduce another
identifier for your value in the non-`A branch :
,----
| # let f = function
|   | `A -> true, `B
|   | `C as x -> false, x ;;
| val f : [< `A | `C ] -> bool * [> `B | `C ] = <fun>
`----
(the [> `B | `C ] return type can be constrained to [`A`B|`C] if you
want)

-- 
   Olivier

Re: [Caml-list] Polymorphic variants question

[Jon Harrop]

On Friday 01 September 2006 18:31, David Allsopp wrote:
> let f x = if x = `A then (true, `B) else (false, x);;

You probably want:

# let f = function `A -> true, `B | `C -> false, `C;;
val f : [< `A | `C ] -> bool * [> `B | `C ] = <fun>

> then I get a type error unless I change
> 	(false, x)
> to
> 	(false, id x)

Use coercion :> instead of an ad-hoc function:

# let (f : [`A | `C] -> bool * [`A | `B | `C]) =
    fun x -> if x = `A then (true, `B) else (false, (x :> [`A|`B|`C]));;
val f : [ `A | `C ] -> bool * [ `A | `B | `C ] = <fun>

> Is there a better way of writing this? I'm using this in the context of
> several interrelated lexers where `A, `B and `C are high-level states and
> certain lexers can only be called in a subset of those states but each
> lexer may yield any value for the next-state. I'd quite like to eliminate
> the id x bit since it's only there to "separate" x from the return value
> for the type-checker.

Note that the type of your id function is not 'a -> 'a:

# let id = function `A -> `A | `C -> `C;;
val id : [< `A | `C ] -> [> `A | `C ] = <fun>

So it accepts a subset of {A, C} and returns a type that unifies with any 
superset of {A, C}.

To leverage static type checking you must provide as much information as 
possible to the static type checker. In this case, rather than using "if" to 
denote `A or not `A, you can just as easily use pattern matching to imply 
specifically `A or `C.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] Polymorphic variants question

[skaller]

On Fri, 2006-09-01 at 18:31 +0100, David Allsopp wrote:

> let f x = if x = `A then (true, `B) else (false, x)

> let (f : [`A | `C] -> bool * [`A | `B | `C]) = fun x -> ...

BTW: when using polymorphic variants I find it is a good idea to:

(a) provide names (aliases, abbreviations) for your types.

(b) annotate function arguments and returns -- if not
   all of them, focus on the top level ones: it's necessary
   for the mli file anyhow.

(c) Prefer

let f x = match x with | ...

over

let f = fun x -> ...

and

let f = function | ..

and in particular for big top level functions like

let f (x:t1):t2 = 
  print_endline ("In Debug " ^ string_of_t1 x);
  let r : t2 = match x with
   ..
  in
  print_endline ("Out Debug " ^ string_of_t2 r);
  r

This shape instruments the input type, output type,
input value and output value.

The thing about polymorphic variants is that because

(a) the typing is structural not nominal (like ordinary variants)

(b) type inference tries to figure out the types from 
  usage scattered through the program

it is not only easy to extend them .. it is easy to
extend them incorrectly .. and the diagnostics from
big variants are horrible :)

Using annotations tends to localise the errors
and give you more information, including Ocaml's
smart trick of using your own alias. (This is very
clever :) It also often reports that you're missing
a particular constructor.

I've been using PM variants for a while now.
I just converted a couple of non-PM ones over.
I kind of like this function, it prints many of
the types I use in my compiler in one function,
almost like overloading :)

let string_of_term dfns term = match term with
  | #qualified_name_t as x -> string_of_qualified_name x
  | #regexp_t as x -> string_of_re x
  | #typecode_t as x -> string_of_typecode x
  | #tpattern_t as x -> string_of_tpattern x
  | #literal_t as x -> string_of_literal x
  | #expr_t as x -> string_of_expr x
  | #pattern_t as x -> string_of_pattern x
  | #statement_t as x -> string_of_statement 0 x
  | #exe_t as x -> string_of_exe 0 x
  | #btypecode_t as x -> string_of_btypecode dfns x

  (* hack .. the type because tbexpr_t is a pair not a variant *)
  | #bexpr_t as x -> string_of_bound_expression dfns (x,`BTYP_void)
  | #bexe_t as x -> string_of_bexe dfns 0 x
  | #ast_term_t as x -> string_of_ast_term 0 x

  (* hack cause we don't know the name *)
  | #symbol_definition_t as x -> string_of_symdef x "unk" [] 

  | #bbdcl_t as x -> string_of_bbdcl dfns x 0
  | #param_kind_t as x -> string_of_param_kind x
  | #property_t as x -> string_of_property x
  | #c_t as x -> string_of_code_spec x
  | #dcl_t as x -> string_of_dcl 0 "unk" (Some 0) [] x
  | #asm_t as x -> string_of_asm 0 x
  | #iface_t as x -> string_of_iface 0 x
  | #access_t as x -> string_of_access x
  | #biface_t as x -> string_of_biface dfns 0 x
  | #btype_qual_t as x -> string_of_bqual dfns x
  | #type_qual_t as x -> string_of_qual x
  | #requirement_t as x -> string_of_raw_req x
  | #ikind_t as x -> string_of_ikind x
  | #named_req_expr_t as x -> string_of_named_req_expr x
  | #raw_req_expr_t as x -> string_of_raw_req_expr x
  | #glr_term_t as x -> string_of_glr_term x

let st dfns term = string_of_term dfns term

This function doesn't DO anything I couldn't already do.
It just saves me worrying what the type of the term is,
and then trying to remember the name of the function that
prints it.

The PM variants let me unify any variants types I'm using,
which is why I converted most of the remaining non-PM
variants over.

Stick with them .. they're worth it!

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Polymorphic variants question

[Andres Varon]

[-- Attachment #1: Type: text/plain, Size: 921 bytes --]


On Sep 1, 2006, at 3:29 PM, skaller wrote:

>
> let string_of_term dfns term = match term with
>   | #qualified_name_t as x -> string_of_qualified_name x

This is, indeed, a practical reason why PM are so nice. In the same  
line of ideas, I wish I could do something like the following :

module type S = sig
	type t
	val f : t -> int
end

module A (B : S with type t = [> ]) (C : S with type t = [> ]) : S  
with type t = [B.t | C.t] = struct
	type t = [ B.t | C.t ]	

	let f x =
		match x with
		| #A.t  as x -> A.f x	
		| #B.t as x -> B.f x
end

Of course the example won't even compile, but I think it reflects the  
spirit of what I would like to do. I know this is just not possible  
due to a practical reason (#A.t is expanded to the constructors that  
it includes, and therefore, A.t has to be fully known at compile  
time, correct?). Is there a theoretical reason to have this  
constraint though?

Andres


[-- Attachment #2: Type: text/html, Size: 2471 bytes --]

Re: [Caml-list] Polymorphic variants question

[Jacques Garrigue]

From: Andres Varon <avaron@gmail.com>
[...]
> In the same line of ideas, I wish I could do something like the
> following :
> 
> module type S = sig
> 	type t
> 	val f : t -> int
> end
> 
> module A (B : S with type t = [> ]) (C : S with type t = [> ]) : S  
> with type t = [B.t | C.t] = struct
> 	type t = [ B.t | C.t ]	
> 
> 	let f x =
> 		match x with
> 		| #A.t as x -> A.f x	
> 		| #B.t as x -> B.f x
> end
> 
> Of course the example won't even compile, but I think it reflects the  
> spirit of what I would like to do. I know this is just not possible  
> due to a practical reason (#A.t is expanded to the constructors that  
> it includes, and therefore, A.t has to be fully known at compile  
> time, correct?). Is there a theoretical reason to have this  
> constraint though?

Just that the concrete type is much simpler.
The abstract type does not work directly, as you need a way to ensure
that B.t and C.t are compatible. Otherwise, one could write

module D = A(struct type t = [ `A of int] ... end)
            (struct type t = [ `A of string] ... end)

which is clearly incorrect.

The good news is that, with Romain Bardou, we have now solved this not
so trivial problem (at least at the theoretical level), so there is
some hope. 
Note however that there are also some more practical problems, and
whether this gets into ocaml or not does not depend only on the
theory...

Jacques Garrigue

Re: [Caml-list] Polymorphic variants question

[Andres Varon]

On Sep 2, 2006, at 7:16 AM, Jacques Garrigue wrote:

> Just that the concrete type is much simpler.
> The abstract type does not work directly, as you need a way to ensure
> that B.t and C.t are compatible. Otherwise, one could write
>
> module D = A(struct type t = [ `A of int] ... end)
>             (struct type t = [ `A of string] ... end)
>
> which is clearly incorrect.

I use a more restricted version of polymorphic variants to ensure  
that two functions that are being composed through a match in the  
style of the question do not share a tag (and so one function will  
not override the expected behavior of the second one), even if the  
tags are fully compatible; being this the case, your example cannot  
occur.

I am not an expert in programming languages, and I cannot see - in  
this restricted case - a reason why that functor could still be  
problematic. Is there some?

Thanks!

Andres

Re: [Caml-list] Polymorphic variants question

[Jacques Garrigue]

From: Andres Varon <avaron@gmail.com>
Subject: Re: [Caml-list] Polymorphic variants question
Date: Sat, 2 Sep 2006 21:22:55 -0400

> 
> On Sep 2, 2006, at 7:16 AM, Jacques Garrigue wrote:
> 
> > Just that the concrete type is much simpler.
> > The abstract type does not work directly, as you need a way to ensure
> > that B.t and C.t are compatible. Otherwise, one could write
> >
> > module D = A(struct type t = [ `A of int] ... end)
> >             (struct type t = [ `A of string] ... end)
> >
> > which is clearly incorrect.
> 
> I use a more restricted version of polymorphic variants to ensure  
> that two functions that are being composed through a match in the  
> style of the question do not share a tag (and so one function will  
> not override the expected behavior of the second one), even if the  
> tags are fully compatible; being this the case, your example cannot  
> occur.
> 
> I am not an expert in programming languages, and I cannot see - in  
> this restricted case - a reason why that functor could still be  
> problematic. Is there some?

Just that I don't see how you could possibly enforce the above
condition either, without something in the signatures to tell the
system that argument sets of B.t and C.t must be disjoint.
Or you are telling me that, as you already included "type t = [B.t |
C.t]" in the return type of the functor, there is already an implicit
constraint on B.t and C.t. This is right indeed, but the point is that
you need some logic to handle this constraint; and you want also to be
able to create unions without necessarily writing it in the outside
signature.

Jacques Garrigue

Re: [Caml-list] Polymorphic variants question

[Andres Varon]

>
> Just that I don't see how you could possibly enforce the above
> condition either, without something in the signatures to tell the
> system that argument sets of B.t and C.t must be disjoint.
> Or you are telling me that, as you already included "type t = [B.t |
> C.t]" in the return type of the functor, there is already an implicit
> constraint on B.t and C.t. This is right indeed, but the point is that
> you need some logic to handle this constraint; and you want also to be
> able to create unions without necessarily writing it in the outside
> signature.
>

I haven't modified the ocaml compiler to be able to make that  
functor, but I have made the small change (or I made a small change  
and left a bunch of holes!), so that unions must always be disjoint,  
you can still use the intersection of type by refining one, but  
unions should always be disjoint (ok, it is turned on with a flag in  
the compiler). This is a desirable feature in the context of my  
program, though I can see that making unions from compatible types is  
also desirable in other contexts.

I want to add exactly the assumption you mention, if type t = [B.t |  
C.t] is included in the type of the functor, that implicit constraint  
is there, otherwise, what will be the proper behavior of the function  
for a tag that appears in both C.t and B.t? one overrides the other?  
It seems to me that in the context of that functor, the union must be  
of disjoint types, not only for that problematic case of yours, but  
even for the compatible cases, otherwise, I cannot guarantee that the  
functor that composes two modules that have even been proved correct,  
will still be correct; if they are disjoint, I clean my hands with  
many problematic corners.

You know far better than me how hard would it be to get this going,  
but I asked because I would like to try to prototype this idea in  
Ocaml, unless there is some flaw that would be induced in the type  
system. It seems to be useful (certainly for me at least :-)).

Thanks!

Andres



> Jacques Garrigue

Re: [Caml-list] Polymorphic variants question

[Jacques Garrigue]

From: Andres Varon <avaron@gmail.com>

> > Just that I don't see how you could possibly enforce the above
> > condition either, without something in the signatures to tell the
> > system that argument sets of B.t and C.t must be disjoint.
> > Or you are telling me that, as you already included "type t = [B.t |
> > C.t]" in the return type of the functor, there is already an implicit
> > constraint on B.t and C.t. This is right indeed, but the point is that
> > you need some logic to handle this constraint; and you want also to be
> > able to create unions without necessarily writing it in the outside
> > signature.
> 
> I haven't modified the ocaml compiler to be able to make that  
> functor, but I have made the small change (or I made a small change  
> and left a bunch of holes!), so that unions must always be disjoint,  
> you can still use the intersection of type by refining one, but  
> unions should always be disjoint (ok, it is turned on with a flag in  
> the compiler). This is a desirable feature in the context of my  
> program, though I can see that making unions from compatible types is  
> also desirable in other contexts.
> 
> I want to add exactly the assumption you mention, if type t = [B.t |  
> C.t] is included in the type of the functor, that implicit constraint  
> is there, otherwise, what will be the proper behavior of the function  
> for a tag that appears in both C.t and B.t? one overrides the other?  
> It seems to me that in the context of that functor, the union must be  
> of disjoint types, not only for that problematic case of yours, but  
> even for the compatible cases, otherwise, I cannot guarantee that the  
> functor that composes two modules that have even been proved correct,  
> will still be correct; if they are disjoint, I clean my hands with  
> many problematic corners.

Interesting point. I'm still convinced that, as polymorphic variants
provide mixed union by opposition to the disjoint union of normal
variants, it would be a pity to restrict them by default.

But since our idea is to add compatibility constraints to functor
parameters, to explicitly allow combining two abstract variant types,
it is actually easy to extend compatibilities with exclusive ones.
That is, to allow mixed sum you would write (omiting the private's)

module A(B : sig type t = [> ] end)(C : sig type t = [> ] ~ [B.t]) = ...

The above  ~ [B.t]  means that C.t should be compatible with C.t
(common tags should have identical types), allowing to create the
union [B.t | C.t].

To accomodate your needs for disjoint sum, we just need a small
variation on that

module A(B : sig type t = [> ] end)(C : sig type t = [> ] ~ [~B.t]) = ...

Here  ~ [~B.t] would mean that C.t shouldn't contain any tag from B.t,
enforcing that they are disjoint. Of course this still allows creating
the union [B.t | C.t].

Jacques Garrigue