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