Re: [Caml-list] Two types of efficiency (Was Efficiency of 'a list)

[John Max Skaller <skaller@ozemail.com.au>]

Olivier Andrieu wrote:

>  John Max Skaller [Sunday 4 May 2003] :
>  > Similarly, subtyping of polymorphic variants is invariant
>  > in the arguments, when covariance is sound and more useful.
>  > This is a real pain for me, since it destroys the main use
>  > I hoped to obtain for polymorphic variants:
>  > 
>  > type x = [`A | `B of x]
>  > type y = [`A | `B of y | `C]
>  > 
>  > x *is* a subtype of y, but the type system
>  > disallows it, failing to recognise that every `B x
>  > of type x is also a `B y of y. Typically I have
>  > say a term for an expression and I want to eliminate
>  > some cases by say a term reduction, but I can't restrict
>  > the resultant type as desired because there's no way
>  > to 'narrow' the type recursion.
> 
> # type x = [`A | `B of x] ;;
> type x = [ `A | `B of x]
> # type y = [`A | `B of y | `C] ;;
> type y = [ `A | `B of y | `C]
> # fun a -> (a :x :> y) ;;
> - : x -> y = <fun>
> 
> Doesn't that mean that x is a subtype of y ?


Indeed. Hmm .. has this changed since 3.04?
[I just installed the CVS version which is 3.06+31 (2003/5/2)]
Let me try a more comprehensible example.


type expr1 = [`Prim | `Add of expr1 * expr1 | `Plus of expr1 * expr1]
type expr2 = [`Prim | `Add of expr2 * expr2]
let lift e = (e : expr2 :> expr1)
;;

let rec r (e:expr1): expr2 =
  match e with
  | `Prim -> `Prim
  | `Add (a,b) -> `Add (r a,r b)
  | `Plus (a,b) -> `Add (r a, r b)
;;

And it works. It didn't before!

So thx for pointing this out, and thx to the
ocaml team for doing this work.

Now I'll go off and try to use it.
It will simplify my code a lot: at present I have a lot
of cases I know won't occur, because they've been
"reduced out" by a prior term rewriting routine, but the typing
didn't allow this to be expressed. A lot of nasty

  | _ -> assert false

terms will be eliminated: getting rid of wildcard
matches should improve compile time error diagnosis
considerably. Kind of a pity I can't write:

type expr1 = [expr2 | `Plus expr1 * expr1]

but it would lift the wrong recursion out.

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850


-------------------
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