This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Polymorphic variants question
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2006-09-01 (19:00) From: skaller Subject: Re: [Caml-list] Re: Polymorphic variants question
```On Fri, 2006-09-01 at 14:33 -0400, Chris King wrote:
> On 9/1/06, David Allsopp <dra-news@metastack.com> wrote:
> > 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?
>
> Yes, you can use the coercion operator to tell the compiler to expand the type of x to include `B:
>
> # let f (x: [`A | `C]) = if x = `A then (true, `B) else (false, (x :> [`A | `B | `C]))
> val f : [ `A | `C ] -> bool * [ `A | `B | `C ] = <fun>
>
> Perhaps someone else can clarify how this accomplishes the same thing as
> your id function, as my understanding of type theory is somewhat rudimentary.

The problem is `C not `B. Looking at this expression:

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

we know the result is a bool followed by:

1. `B in the true case
2. x in the false case

But we know x might be `A from the comparison

x = `A

so now we know the result is bool followed by `A, `B,
or something else, we know not what, which x might be.

Note that the type of x must include the case `A,
since if this were not so the comparison:

x = `A

could not be between the same types .. even though x is
only returned when it is *not* `A -- that's a flow
of control issue not a typing issue.

By using:

let id = function `A -> `A | `C -> `C

the compiler knows (id x) can include `A
and it can include `C, the case

(true, `B)

being returned says the return type can also be `B.
So the return type can be bool followed by `A, `B,  or `C.

Hope that makes sense :)

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

```