[Caml-list] Getting rid of impossible polymorphic variant tags from infered types

[Caml-list] Getting rid of impossible polymorphic variant tags from infered types

[Florian Hars]

If I write a function to filter out all occurences of values of a specific 
polymorphic variant tag from a list, ocaml infers a return type for this 
function of any type that may contain the tag I have just removed:

# let f l = List.filter (function `Fnord -> false | _ -> true) l;;
val f : ([> `Fnord] as 'a) list -> 'a list = <fun>

While I unterstand why this type is infered, it is nonetheless wrong, it should 
be something like [> 'a \ `Fnord ] list (inventing notation on the fly).
Is there some decent way to tell the compiler that I know more about this 
function than the type checker does?

The following should be safe, but doesn't strike me as especially elegant and 
makes the type more restrictive than I'd like it to be:

type foo = [ `Foo | `Bar | `Fnord ]
type foo_flat = [ `Foo | `Bar ]

let f' l =
   let f_r (v: foo) (init: foo_flat list) =
     match v with
     | `Fnord -> init
     | _ -> Obj.magic v :: init
   in
   List.fold_right f_r l []

Yours, Florian.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Getting rid of impossible polymorphic variant tags from infered types

[Claudio Sacerdoti Coen]

> type foo = [ `Foo | `Bar | `Fnord ]
> type foo_flat = [ `Foo | `Bar ]
> 
> let f' l =
>   let f_r (v: foo) (init: foo_flat list) =
>     match v with
>     | `Fnord -> init
>     | _ -> Obj.magic v :: init
>   in
>   List.fold_right f_r l []

 There is no need for Obj.magic:

type foo_flat = [ `Foo | `Bar ]
type foo = [ foo_flat | `Fnord ]
let f_r (v : foo) (init : foo_flat list) =
 match v with
   `Fnord -> init
 | #foo_flat as v -> v :: init
 ;;
type foo = [ `Bar | `Fnord | `Foo ]
type foo_flat = [ `Bar | `Foo ]
val f_r : foo -> foo_flat list -> foo_flat list

 Since the list `Foo | `Bar of variants is written only once,
 the code is also reasonably extensible. Of course it is still not
 what you want.




 If you really need to exclude the `Fnord value at compile time, an
 alternative solution is to use phantom types:

type 'a foo = [ `Foo | `Bar | `Fnord ]
let f_r (v : 'a foo) (init : ([> `NoFnord] foo) list) =
 match v with
   `Fnord -> init
 | _ -> v :: init
 ;;
type 'a foo = [ `Bar | `Fnord | `Foo ]
val f_r : 'a foo -> ([> `NoFnord ] as 'b) foo list -> 'b foo list

The `NoFnord variant explicitly tells that the Fnord value is not allowed.
Notice how the first parameter does not have to satisfy this restriction,
while the second one has to. As usual, you need to use modules to enforce
that a value of type `Foo has type [`NoFnord] foo whereas a value of type
`NoFnord has NOT type [`NoFnord].

					Regards,
					C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Getting rid of impossible polymorphic variant tags from infered types

[Florian Hars]

Claudio Sacerdoti Coen wrote:
>  If you really need to exclude the `Fnord value at compile time, an
>  alternative solution is to use phantom types:
> 
> type 'a foo = [ `Foo | `Bar | `Fnord ]
> let f_r (v : 'a foo) (init : ([> `NoFnord] foo) list) =
>  match v with
>    `Fnord -> init
>  | _ -> v :: init
>  ;;

But this gives me the worst of both worlds, no? I have to define a function f_r 
for every type I might want to use in place of foo, *and* the type checker can 
still see the `Fnord that isn't there:

# let l' = List.fold_right f_r [`Fnord; `Foo; `Bar] [] ;;
val l' : _[> `NoFnord] foo list = [`Foo; `Bar]
# match List.hd l' with
   | `Foo -> print_endline "Foo!"
   | `Bar -> print_endline "Bar!";;
This pattern matches values of type [< `Bar | `Foo]
but is here used to match values of type
   [> `NoFnord] foo = [ `Bar | `Fnord | `Foo]
The first variant type does not allow tag(s) `Fnord

So the "| #foo_flat as v -> v :: init" version seems to be the only workable 
solution.

Yours, Florian.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Getting rid of impossible polymorphic variant tags from infered types

[Claudio Sacerdoti Coen]

> But this gives me the worst of both worlds, no?

 It is a bit heavyweight, but not too bad.

> I have to define a function 
> f_r for every type I might want to use in place of foo,

 Wasn't it your goal to define f_r in the first place?

> *and* the type checker can still see the `Fnord that isn't there:

 You are right here. Indeed, you should define your own case-analysis
 operator (whose principal argument would have type [> `NoFnord] foo)
 and use it in place of the match ... with.
 Withouth proper syntax sugar the code becomes clumsy.
 This is a drawback of phantom types.

> So the "| #foo_flat as v -> v :: init" version seems to be the only 
> workable solution.

					Regards,
					C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners