[Caml-list] Polymorphic variants

[Caml-list] Polymorphic variants

[John Max Skaller]

I've been using polymorphic variants for a little while, and am
interested in their current status. Here are some comments. The 
executive summary is:
they're definitely worth using, and definitely worth continued
development.

My project is a compiler. The main reason I switched to
polymorphic variants is that term desugaring and reductions
would appear to be best handled by a single large term type,
and a various subsets appropriate to context. For example,
a type expression is a subset of an expression: it admits
addition, multiplication and exponentiation, but no
subtraction.

Unfortunately, this doesn't work out as well as I'd expected
because of recursion:

type a = [`A of a  | `B]
type b = [`A of  b]

The second type is a subtype of the first,
but this fails:

let f (x:a) =
match x with
  #b -> ()

with the message:

This pattern matches values of type [< b] = [< `A of b]
but is here used to match values of type a = [ `A of a | `B];;

Ocaml understands subtyping by subsets of variants,
but the constructor arguments must be invariant.
The work around is to decode the argument manually,
but then one wonders what the gain over standard variants is.
Here is another example:

 type x = [`A of int | `A of float];;
This variant type contains a constructor [ `A of float] which should be
[ `A of int]

No, I meant what I said! I can write both:

`A 1

and also

`A 1.1

and I am trying  to tell the compiler they both belong
to type x. It has no right to complain here. Of course,
this does lead to a problem:

 match x with | `A a -> ..

what type is a? It's 'a initially,
and bound on the first use. Which makes
matching on first `A 1 and then `A 1.1
impossible.  This is a problem with the ocaml type
inference mechanism not my type declaration!
[So it can't deduce the type of a .. but I could specify it
if there were syntax like

| `A (a:int) -> ...

[It seems to me that the type of the argument
is taken *incorrectly* as the intersection
type int & float, when it is actually a sum..
in the case of a sum the constraint would be
enough to fix the type correctly .. on the other hand,
intersections would correctly solve the covariance
problem .. ??]

In fact I found the type inference
engine stumbled around over legitimate matches,
and some extra help in the form of function argument
type  constraints was necessary (a small price to pay,
but worth noting an example in the manual).

In any case, polymorphic variant constructors really
ARE overloaded, but when it comes to declaring
types, overloading isn't allowed. This is an anomaly ..
and it hit me quite hard initially, because of the natural
attempt to try to use covariant arguments.

A second problem I found is the verbose error messages.
When you have 20 variants, a mismatch is a real pain
to decypher. It would be useful if variants HAD to be
declared like:

variant `A of int
variant `A of float
variant `B of long

so that spelling mistakes and type errors in constructor
arguments could be more easily pinpointed .. but of course,
this can't work due to recursion ... hmmm...

One thing that *definitely* needed improvement is the syntax
for declaring types: having to repeat all the cases every time
is an error prone tedium. It appears this HAS been done in
ocaml 3.04! THANK YOU!! One can now write:

type a = [`A]
type b = [`B]
type c = [a | b]

[#types were previously allowed in pattern matches but not
type declarations ..]

Well, are polymorphic variants worth the effort?
I think they are: they're not perfect, they're certainly
more error prone than standard variants .. but they're
also a lot more expressive and save considerable
coding, and in many cases they're much faster as well.
[In particular, injecting a subset of cases into a supertype
is a no-operation, whereas standard variants require
actually building new values]


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

Re: [Caml-list] Polymorphic variants

[Remi VANICAT]

John Max Skaller <skaller@ozemail.com.au> writes:

> Unfortunately, this doesn't work out as well as I'd expected
> because of recursion:
> 
> type a = [`A of a  | `B]
> type b = [`A of  b]
> 
> The second type is a subtype of the first,
> but this fails:
> 
> let f (x:a) =
> match x with
>   #b -> ()
> 
> with the message:
> 
> This pattern matches values of type [< b] = [< `A of b]
> but is here used to match values of type a = [ `A of a | `B];;


the problem here is that you intended #b is a non fixed matching rule,
I mean, imagine you have :

`A (`A ( `A ( `A ( `A ( `A `B)))))

to check that this is not in #b, one have to look deep in the
structure of the value. pattern matching only look at the firsts
levels of the structure. This must be done otherwise. for example :

type a = [`A of a | `B | `C]
type b = [`A of b | `C]

let rec f (x:a) =
  match x with
  | `A x -> `A (f x)
  | `C -> `C
  | _ -> failwith "arg";;

> 
> Ocaml understands subtyping by subsets of variants,
> but the constructor arguments must be invariant.
> The work around is to decode the argument manually,
> but then one wonders what the gain over standard variants is.
> Here is another example:
> 
>  type x = [`A of int | `A of float];;
> This variant type contains a constructor [ `A of float] which should be
> [ `A of int]
> 
> No, I meant what I said! I can write both:
> 
> `A 1
> 
> and also
> 
> `A 1.1

No, you can't. the types informations are lost at runtime, so ocaml
will never be able to make the difference between the two.

> 
> and I am trying  to tell the compiler they both belong
> to type x. It has no right to complain here. Of course,
> this does lead to a problem:
> 
>  match x with | `A a -> ..
> 
> what type is a? It's 'a initially,
> and bound on the first use. Which makes
> matching on first `A 1 and then `A 1.1
> impossible.  

it won't be enough, to fail to match this, ocaml should be able to
know type at runtime. Type doesn't not exist at runtime

> This is a problem with the ocaml type
> inference mechanism not my type declaration!
> [So it can't deduce the type of a .. but I could specify it
> if there were syntax like
> 
> | `A (a:int) -> ...
> 
> [It seems to me that the type of the argument
> is taken *incorrectly* as the intersection
> type int & float, when it is actually a sum..
> in the case of a sum the constraint would be
> enough to fix the type correctly .. on the other hand,
> intersections would correctly solve the covariance
> problem .. ??]
> 
> In fact I found the type inference
> engine stumbled around over legitimate matches,
> and some extra help in the form of function argument
> type  constraints was necessary (a small price to pay,
> but worth noting an example in the manual).
> 
> In any case, polymorphic variant constructors really
> ARE overloaded, but when it comes to declaring
> types, overloading isn't allowed. This is an anomaly ..
> and it hit me quite hard initially, because of the natural
> attempt to try to use covariant arguments.
> 
> A second problem I found is the verbose error messages.
> When you have 20 variants, a mismatch is a real pain
> to decypher. It would be useful if variants HAD to be
> declared like:
> 
> variant `A of int
> variant `A of float
> variant `B of long
> 
> so that spelling mistakes and type errors in constructor
> arguments could be more easily pinpointed .. but of course,
> this can't work due to recursion ... hmmm...
> 
> One thing that *definitely* needed improvement is the syntax
> for declaring types: having to repeat all the cases every time
> is an error prone tedium. It appears this HAS been done in
> ocaml 3.04! THANK YOU!! One can now write:
> 
> type a = [`A]
> type b = [`B]
> type c = [a | b]
> 
> [#types were previously allowed in pattern matches 

it's not type in pattern matching, it's pattern. It is not, at all,
the same thing, even if their is link between the two.

> but not type declarations ..]

not exactly :


type foo = [ 'BAR ]
type 'a t = 'a constraint 'a = #foo;;

is correct, but deprecated, one should use :

type 'a t = 'a constraint [< foo] = 'a;;

> 
> Well, are polymorphic variants worth the effort?
> I think they are: they're not perfect, they're certainly
> more error prone than standard variants .. but they're
> also a lot more expressive and save considerable
> coding, and in many cases they're much faster as well.
> [In particular, injecting a subset of cases into a supertype
> is a no-operation, whereas standard variants require
> actually building new values]

You should look to the mixin.ml file that can be found in testlabl
directories of the source distribution, it show how to make what you
seem to want.
-- 
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat
-------------------
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] Polymorphic variants

[John Max Skaller]

Remi VANICAT wrote:

>John Max Skaller <skaller@ozemail.com.au> writes:
>
>>Unfortunately, this doesn't work out as well as I'd expected
>>because of recursion:
>>
>>type a = [`A of a  | `B]
>>type b = [`A of  b]
>>
>>The second type is a subtype of the first,
>>but this fails:
>>
>>let f (x:a) =
>>match x with
>>  #b -> ()
>>
>>with the message:
>>
>>This pattern matches values of type [< b] = [< `A of b]
>>but is here used to match values of type a = [ `A of a | `B];;
>>
>
>the problem here is that you intended #b is a non fixed matching rule,
>I mean, imagine you have :
>
>`A (`A ( `A ( `A ( `A ( `A `B)))))
>
>to check that this is not in #b, one have to look deep in the
>structure of the value. 
>
Yes. But high level programming languages are *meant* to do
high level things, aren't they?

Here's another example that fails, which is very annoying:

type a = [`A of e | `B]
and e = [a  | `C]

"The type constructor a is not yet completely defined"

Arggg. Of course it isn't. It works just fine if I textually
substitute:

type a =[`A of e | `B]
and e = [`A of e|`B|`C]

Almost all interesting cases of variants (for compiler writers anyhow)
involve type recursion. It shouldn't matter if the type is completely
defined, only that the definition is finally completed :)

BTW: I can't write  "t as x" in a type expression. Why not?
I'm forced to name it in a type binding .. that means that inductive types,
for example, can not be specified anonymously:

  (Cons of list | Empty) as list

Yeah, ocaml sum types are generative ... but the polymorphic
variant equivalents are not .. so

  [`Cons of list | `Empty] as list

should work. [Can I use a 'constraint' here? I've never used
a constraint before]

>pattern matching only look at the firsts
>levels of the structure. This must be done otherwise.
>
It doesn't "must" be done. I think you mean, there are advantages
only handling the easy cases: easy to write the compiler,
easy to optimise, easy for the end user to monitor
code complexity .. and easy for the programmer to handle
the more difficult cases manually ..

> for example :
>
>type a = [`A of a | `B | `C]
>type b = [`A of b | `C]
>
>let rec f (x:a) =
>  match x with
>  | `A x -> `A (f x)
>  | `C -> `C
>  | _ -> failwith "arg";;
>

The compiler doesn't know the type of x here,
at least without looking at the usage (clearly, usage
dictates type a). But the ambiguity could easily
be resolved by the client with an annotation.

>>
>>No, I meant what I said! I can write both:
>>
>>`A 1
>>
>>and also
>>
>>`A 1.1
>>
>
>No, you can't. the types informations are lost at runtime, so ocaml
>will never be able to make the difference between the two.
>
I certainly can write them both:

`A 1; `A 1.1;
type int_t = [`A of int];
type float_t = [`A of float];;

No problem doing this. Perhaps there should be.
The problem only manifests here:

type num = [ int_t | float_t ]

because the same constructor name has two different
argument types. It is even possible to write a function
that accepts both

let f x = x

happily accepts both :-)

Now you say that the type information is lost at run time,
but that is NOT immediately apparent from the documentation.
Indeed, it need not be the case: the implementation *could*
mangle the constructor name with the argument type
so that

  `A_int
  `A_float

are treated as distinct constructors. Then the following:

fun x = match x with
| `A a -> ..

would give an error, since the compiler cannot know
which `A it is, however the problem could easily be fixed
by the user:

| `A (a:int) ->

now we know it is `A of int. Things "must be so"
if they are a consequence of theory, but it isn't
always evident which theory is used, and why that
one is best :-)

Perhaps one consequence of this is that the documentation
needs to be more specific and have more examples:
the author knowing the chosen theory and implementation
believes only lightweight coverage is necessary, not seeing
the many alternatives someone less involved might.

For example, C++ objects DO have associated and accessible
run time type information. I know Ocaml doesn't .. but there are
other things I know less well, and there are C++ users
coming to ocaml that might think pattern matching
uses RTTI.

To come back to the examples: the type

[`A of int | `A of float | `B]

is perfectly legitimate. The actual error is only on matching.
If the client never matches on `A, there is no error:

match x with | `B -> .. | _ -> ...

this match would be OK, `A isn't refered to.
It isn't clear why the compiler writer chose to allow
any argument of `A, but disallows specifying a name for
a type containing two distinct `A constructors instead
of simply reporting an ambiguity on use: they're
called "polymorphic variants" but they aren't actually polymorphic,
at least in this sense :-)


>
>it's not type in pattern matching, it's pattern. It is not, at all,
>the same thing, even if their is link between the two.
>
Sure, I know that. (Actually, the sum constructor tags really ARE
run time type information, they tell which case of the sum
is represented, and hence the type of the constructor argument)

>
>You should look to the mixin.ml file that can be found in testlabl
>directories of the source distribution, it show how to make what you
>seem to want.
>
The biggest problem I have with ocaml, is that while I can
make anything I want, it is often not evident just what the
compiler/language permits, and what it doesn't.

This is particularly serious for me when it comes to modules:
it just isn't clear to me what will work and what will not,
and experiments here can be very time consuming and laborious.
The ideas seem simple, but the syntax is sometimes quite arcane,
and all sorts of restrictions that don't exist in the underlying
basic category theory can bite you days into a project.

To give a more concrete example: the first time I tried to
use polymorphic variants, I lost a week and had to undo
all my changes because I kept getting error messages I
couldn't make head or tail of. I decided to try again
when my project got even more complex, and I really needed
stronger static typing, but didn't want to create a huge number
of standard sum types and laboriously code the maps between
them case by case .. not to mention the industrial requirement
that every type have an associated print routine, for example.

I pressed on despite the horrendous error messages,
knowing that the transormation HAD to be totally
mechanical in the first instance. [Replace A with `A ..]

I lost another week due to a bug in Ocaml 3.02.
It took a while to determine this really was a compiler bug
matching polymorphic variants (3.01 worked fine,
and so does 3.04).

[My point is that it is very hard to proceed when you don't
know if an error is a bug in your understanding, a bug
in your implementation, or a bug in the compiler ..
so it is safer to eliminate the first case by not using
advanced features .. but if this argument were extended,
it would be an argument for using C instead of ocaml...]

Well, having looked at the English translation of the 
Ocaml book by Emmanuel Chailloux, Pascal
Manoury and Bruno Pagano, I think a big hole is going
to be plugged. This book covers quite advanced topics,
I might learn something here!

Anyhow .. sadly, ocaml is such a wonderful language.
I say sadly because I am unemployed and poor .. and
just can't bring myself to work with C/C++ again.
Its just too much of a step backwards, and I'm not
enough of a diplomat to hide it from my fellow
workers or employers (who still think OO and C++
are wonderful, and Java is Gods own language ..)

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

Re: [Caml-list] Polymorphic variants

[Jacques Garrigue]

From: John Max Skaller <skaller@ozemail.com.au>
> Remi VANICAT wrote:
> 
> >John Max Skaller <skaller@ozemail.com.au> writes:
> >
> >>Unfortunately, this doesn't work out as well as I'd expected
> >>because of recursion:
> >>
> >>type a = [`A of a  | `B]
> >>type b = [`A of  b]
> >>
> >>The second type is a subtype of the first,
> >>but this fails:
> >>
> >>let f (x:a) =
> >>match x with
> >>  #b -> ()
> >>
> >>with the message:
> >>
> >>This pattern matches values of type [< b] = [< `A of b]
> >>but is here used to match values of type a = [ `A of a | `B];;
> >>
> >
> >the problem here is that you intended #b is a non fixed matching rule,
> >I mean, imagine you have :
> >
> >`A (`A ( `A ( `A ( `A ( `A `B)))))
> >
> >to check that this is not in #b, one have to look deep in the
> >structure of the value. 
> >
> Yes. But high level programming languages are *meant* to do
> high level things, aren't they?

The only problem is that you're asking for potentially non-terminating
computation to be done during pattern-matching. No, Caml is not
Haskell.
By the way, you can of course do that with a when clause.
Unfortunately, if you want to coerce the value to be a "b", this will
force you to rebuild your value, but anyway you have to access all
leaves of your value before knowing whether it is actually a "b" or
not.
Note that it might be simpler to have most of your functions defined
for "a" rather than for "b", and coerce from "b" to "a":
  (_ : b :> a)
Note the double coercion here, (_ :> a) wouldn't work.

> Here's another example that fails, which is very annoying:
> 
> type a = [`A of e | `B]
> and e = [a  | `C]
> 
> "The type constructor a is not yet completely defined"

But your example is not recursive.
You can just write
  type e = [a | `C]
and it will work fine.

> Almost all interesting cases of variants (for compiler writers anyhow)
> involve type recursion. It shouldn't matter if the type is completely
> defined, only that the definition is finally completed :)

Yes, it matters. Because a variant is a flat type, and the definition
of a variant type depends on the definition of its parts.
Of course it would be possible to do a topological sort to search where
there is no recursion, and remove the recursion automatically.
But this doesn't seem to be the ML approach for values either, and it
wouldn't add any expressive power.

> BTW: I can't write  "t as x" in a type expression. Why not?
> I'm forced to name it in a type binding .. that means that inductive types,
> for example, can not be specified anonymously:
>
>   [`Cons of list | `Empty] as list
> 
> should work. [Can I use a 'constraint' here? I've never used
> a constraint before]

Yes you can. Wasn't it in the tutorial:

    [`Cons of 'list | `Empty] as 'list

> >pattern matching only look at the firsts
> >levels of the structure. This must be done otherwise.
> >
> It doesn't "must" be done. I think you mean, there are advantages
> only handling the easy cases: easy to write the compiler,
> easy to optimise, easy for the end user to monitor
> code complexity .. and easy for the programmer to handle
> the more difficult cases manually ..

Not only that: easily understandable properties. This is the most
important part.

> I certainly can write them both:
> 
> `A 1; `A 1.1;
> type int_t = [`A of int];
> type float_t = [`A of float];;
> 
> No problem doing this. Perhaps there should be.

There is no problem as long as these cases are used independently.
But you cannot mix them in the same variant type.
How are we going to build a model of [`A of int | `A of float].
Basically this suppose that we are able to build the union set of
ints and floats. All the type theory theory of ML is based on the fact
that there is no such set/type.

> Now you say that the type information is lost at run time,
> but that is NOT immediately apparent from the documentation.
> Indeed, it need not be the case: the implementation *could*
> mangle the constructor name with the argument type
> so that
> 
>   `A_int
>   `A_float
> 
> are treated as distinct constructors. Then the following:
> 
> fun x = match x with
> | `A a -> ..
> 
> would give an error, since the compiler cannot know
> which `A it is

What this basically means is that any use of `A without type
annotation should generate an error. The whole point of polymorphic
variants being that they are independent from definitions, I really
cannot follow you here.

Sorry, but the feature you are asking for is not polymorphic variants.
This looks more like tree automata types, like they have for XML
typing. This indeed allows for all strange inclusions and unions, but
you can forget about type inference. These are interesting for
themselves, but how to mix them with languages with type inference is
still an open problem.

> Things "must be so" if they are a consequence of theory, but it
> isn't always evident which theory is used, and why that one is best
> :-)

Read the papers :-)
There is a whole literature about lambda-calculus, type systems,
models...
One trouble is that it is hard to explain all this theory in a few
lines.

> Perhaps one consequence of this is that the documentation
> needs to be more specific and have more examples:
> the author knowing the chosen theory and implementation
> believes only lightweight coverage is necessary, not seeing
> the many alternatives someone less involved might.

You're probably right. But your remark also describes the basic
problem: as long as the author is the only one to document a feature,
his description will only be partial.

> To come back to the examples: the type
> 
> [`A of int | `A of float | `B]
> 
> is perfectly legitimate. The actual error is only on matching.
> If the client never matches on `A, there is no error:
> 
> match x with | `B -> .. | _ -> ...
> 
> this match would be OK, `A isn't refered to.
> It isn't clear why the compiler writer chose to allow
> any argument of `A, but disallows specifying a name for
> a type containing two distinct `A constructors instead
> of simply reporting an ambiguity on use: they're
> called "polymorphic variants" but they aren't actually polymorphic,
> at least in this sense :-)

Polymorphism being a subtle thing...
The polymorphism in variants only describes the fact they can be built
from a bunch of constraints, rather than being defined in advance.

Also, the type you are talking about is

  [< `A of int | `A of float | `B]

which is perfectly legitimate (in the current theory).
You can even name it:

  type 'a t = 'a constraint 'a = [< `A of int | `A of float | `B]

This type being polymorphic, you need to leave a variable to expose
this polymorphism.

On the other hand,
  [`A of int | `A of float | `B]
is the intersection of the above type and
  [> `A of int | `A of float | `B]
This last type is illegal, because you wouldn't be able to match such
a type.

Note that one could think of ways to make the above legal, using
intersection rather than union, but I don't see how it would be
useful, because you would have no way to access the value anyway.
Like throwing data into a black hole.

> >it's not type in pattern matching, it's pattern. It is not, at all,
> >the same thing, even if their is link between the two.
> >
> Sure, I know that. (Actually, the sum constructor tags really ARE
> run time type information, they tell which case of the sum
> is represented, and hence the type of the constructor argument)

They tell more: you may have several cases with the same type.

> Well, having looked at the English translation of the 
> Ocaml book by Emmanuel Chailloux, Pascal
> Manoury and Bruno Pagano, I think a big hole is going
> to be plugged. This book covers quite advanced topics,
> I might learn something here!

This is indeed a nice book, but written before the introduction of
polymorphic variants. So almost nothing about them in it.

Actually, this is one reason I would want to say: now polymorphic
variants are finished, let's work with them, and try to describe what
they can do. This is too hard to do that on a moving target.

Cheers,

Jacques
-------------------
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] Polymorphic variants

[John Max Skaller]

Jacques Garrigue wrote:

>>BTW: I can't write  "t as x" in a type expression. Why not?
>>I'm forced to name it in a type binding .. that means that inductive types,
>>for example, can not be specified anonymously:
>>
>>  [`Cons of list | `Empty] as list
>>
>>should work. [Can I use a 'constraint' here? I've never used
>>a constraint before]
>>
>
>Yes you can. Wasn't it in the tutorial:
>
>    [`Cons of 'list | `Empty] as 'list
>
Argg. Sorry. Of course, I used a plain identifier instead of a type 
variable.

>>It doesn't "must" be done. I think you mean, there are advantages
>>only handling the easy cases: easy to write the compiler,
>>easy to optimise, easy for the end user to monitor
>>code complexity .. and easy for the programmer to handle
>>the more difficult cases manually ..
>>
>
>Not only that: easily understandable properties. This is the most
>important part.
>
Yes, but it is an amorphous thing. The specification
of an 'integer' is easily understandable. Only, the greatest
minds in mathematics struggle to know what a prime
number is.

>>I certainly can write them both:
>>
>>`A 1; `A 1.1;
>>type int_t = [`A of int];
>>type float_t = [`A of float];;
>>
>>No problem doing this. Perhaps there should be.
>>
>
>There is no problem as long as these cases are used independently.
>But you cannot mix them in the same variant type.
>
Yeah, I know .. but it isn't clear from the manual,
perhaps because this very example is not included in it.

>
>How are we going to build a model of [`A of int | `A of float].
>Basically this suppose that we are able to build the union set of
>ints and floats. All the type theory theory of ML is based on the fact
>that there is no such set/type.
>
Not at all. Felix does this, just fine. And I'm no type theorist.
But the algorithms work. I'm not saying ocaml should do
what I did in Felix, but there is no problem at all building
a model, `A is just a function, and in Felix functions
can be overloaded. Including variant constructors.
[These are classic ML style unions, not open ones
like polymorphic variants: they have to be declared
or it wouldn't work]

In Felix, it is fine to duplicate not just constructors,
but any function type:

fun f:x->y = ..
fun f:x->y= ..

No problem. But here:

print (f x);

there is a problem: which f to use?

Is this a good design decision? I don't know: I *could*
report a duplicate definition (and I *do* for duplicate
things other than than functions).

But there is evidence that this IS a good design
decision, it comes from overloading templates
in C++. Since a template basically models a family
of functions, two tempates often model the same
type .. and it would be really silly to ban the templates
because of this. Instead, an error is reported only
when a particular instantiation is ambiguous.

I'm not criticizing the decisions made for polymorphic
variants, just pointing out that a lot of alternatives
do exist, and it would be useful to see an explanation
of why the various interesting nasty cases are
handled the way they are.

>
>What this basically means is that any use of `A without type
>annotation should generate an error. The whole point of polymorphic
>variants being that they are independent from definitions, I really
>cannot follow you here.
>
Nor I you. When the compiler sees:

    `A 1

in an expression then it silently replaces it with


    `A_int 1

so that the actual constructor name is distinct for every argument type.
This is called 'name mangling' and C++ compilers do it all the time
to every external function symbol in a program.

In a pattern match, there is a problem because the mangling
cannot be done when the expression being decoded
is of a type with two constructor of the same unmangled name.
So in this case ONLY, the client must disambiguate by
specifying which type is meant:

    `A (x:int)


is replaced by

  `A_int x

>
>Sorry, but the feature you are asking for is not polymorphic variants.
>

I am NOT asking for it. I am merely critiquing it from the point
of view of a user. Remember, I am using them: the whole of my
compiler uses polymorphic variants extensively and almost
exclusively (only a few of the traditional sum types remain
in a couple of places because there is no point replacing them).
So you could say I'm a fairly heavy user of them :-)

>>Things "must be so" if they are a consequence of theory, but it
>>isn't always evident which theory is used, and why that one is best
>>:-)
>>
>
>Read the papers :-)
>There is a whole literature about lambda-calculus, type systems,
>models...
>One trouble is that it is hard to explain all this theory in a few
>lines.
>
And the other is that there are a LOT of theories.

Furthermore, the theory upon which an implementation
is based doesn't determine all the technical design decisions:
like, for example, whether to report that a type with duplicate
constructors is an error even if it isn't used, or whether
to defer the error to the point of use .. and provide a disambiguation
mechanism.

C++ for example, adopts BOTH of these philosophies in different
places, which is one reason it is a mess.

>>Perhaps one consequence of this is that the documentation
>>needs to be more specific and have more examples:
>>the author knowing the chosen theory and implementation
>>believes only lightweight coverage is necessary, not seeing
>>the many alternatives someone less involved might.
>>
>
>You're probably right. But your remark also describes the basic
>problem: as long as the author is the only one to document a feature,
>his description will only be partial.
>
So add in the example I gave? I can't do that, I don't have access to the
document source. But I have 'documented' it in the email :-)

>
>Note that one could think of ways to make the above legal, using
>intersection rather than union, but I don't see how it would be
>useful, because you would have no way to access the value anyway.
>Like throwing data into a black hole.
>
The pragmatics of programming often require useless things.
For example, unreachable code .. because the programmer
has commented something out. Empty types (why was []
removed??) because they're yet to be filled in with cases,
but we want to name the type anyhow, perhaps to write
a function signature ..

The unit type. It is theoretically useless in a (purely) functional
programming language. Why is it there?

>>Well, having looked at the English translation of the 
>>Ocaml book by Emmanuel Chailloux, Pascal
>>Manoury and Bruno Pagano, I think a big hole is going
>>to be plugged. This book covers quite advanced topics,
>>I might learn something here!
>>
>
>This is indeed a nice book, but written before the introduction of
>polymorphic variants. So almost nothing about them in it.
>
>Actually, this is one reason I would want to say: now polymorphic
>variants are finished, let's work with them, and try to describe what
>they can do. This is too hard to do that on a moving target.
>

Well, I'm doing my part: I'm using them all the time,
and I'm relating my experience so you can get some feeling
for how someone else views them that is. I was hoping
to get much stronger static typing using them. In fact,
I have better typing, but nowhere near as strong as I
either expected initially, or would like.

Some of the typing I'd like is plain impossible.
And some is inconvenient to implement, or too quirky
to bother with. And some is desirable but not implemented
or not understood. And I don't really know the distinction
between all these cases.

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

[Caml-list] How to compare recursive types?

[John Max Skaller]

How to compare recursive types?
[Or more generally, datya structures ..]

Here is my best solution so far.
For sake of argment types are either

  a) primitive
  b) binary product
  c) typedef (alias) name

Suppose there is an environment

typedef t1 = ...
typedef t2 = ...
typedef t3 ....

and two type expression e1 and e2

We compare the type expressions structurally and recursively,
also passing a counter value:

  cmp 99 e1 e2

When we reach a typedef name,
we decrement the counter argument. 

If the counter drops
to zero, we return true, otherwise we 
replace the name by the expression it denotes
and continue (using the decremented counter).

It is "obvious" that for a suitably large counter,
this algorithm always terminates and gives the
correct result. [The proof would follow from
some kind of structural induction]

Q1: is there a better algorithm? What does Ocaml use?

Q2: how to estimate the initial value of the counter?

I guess that, for example, 2(n +1) is enough for the counter,
where n is the number of typedefs in the environment.

My argument is in two parts:

A. if we don't get a recursion after
substituting each typedef (while chasing down a branch
of the tree), we can't get it at all.

B. The fixpoint of a branch of the second expression must be somewhere
between the recursion target of the first fixpoint of the
equivalent branch of the first expression and the second one.
In other words, it is always enough to expand the fixpoint
twice in one expression (along a single branch), 
any more expansions are sure to follow
exactly the same behaviour as has already been performed.

Q3: the same issue must arise in implementing the ocaml
structural comparison function. Is there a way to
build the data structures (factor out the typedefs)
so i can use it directly on the terms?

Q4: Is there a way to minimise the representation?

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

Re: [Caml-list] How to compare recursive types?

[Andreas Rossberg]

This is highly off-topic, but anyway...

John Max Skaller wrote:
> 
> How to compare recursive types?
> [Or more generally, datya structures ..]
> 
> Here is my best solution so far.
> For sake of argment types are either
> 
>   a) primitive
>   b) binary product
>   c) typedef (alias) name

OK, so you don't have type lambdas (parameterised types). In that case
any type term can be interpreted as a rational tree. There are standard
algorithms for comparing such trees, they are essentially simple graph
algorithms. Something along these lines is used in the OCaml compiler.

If you add lambdas (under recursion) things get MUCH harder. Last time I
looked the problem of equivalence of such types under the equi-recursive
interpretation you seem to imply (i.e. recursion is `transparent') was
believed to be undecidable.

> We compare the type expressions structurally and recursively,
> also passing a counter value:
> 
>   cmp 99 e1 e2
> 
> When we reach a typedef name,
> we decrement the counter argument.
>
> If the counter drops
> to zero, we return true, otherwise we
> replace the name by the expression it denotes
> and continue (using the decremented counter).

So you return true for any infinite (i.e. recursive) type.
Interesting...

Seriously, what do you mean by "reaching a typedef name"? In one
argument? In both simultanously? What if you reach different names? From
the second paragraph it seems that you have only considered one special
case. For the others, if your counter dropped to 0, you had to return
false for the sake of termination, which renders the algorithm incorrect
(or incomplete, if you want to put it mildly).

> It is "obvious" that for a suitably large counter,
> this algorithm always terminates and gives the
> correct result. [The proof would follow from
> some kind of structural induction]

I doubt that ;-) In fact it is obvious that your algorithm is incorrect.
[The proof is a simple counter example like (cmp n t1 t2) where
t1=prim*t1, t2=prim*t2.]

Regards,

	- Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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] How to compare recursive types?

[Haruo Hosoya]

Dear Andreas,

I'm juping in the middle of the discussion (not following the
context)...

Andreas Rossberg <rossberg@ps.uni-sb.de> wrote:

> If you add lambdas (under recursion) things get MUCH harder. Last time I
> looked the problem of equivalence of such types under the equi-recursive
> interpretation you seem to imply (i.e. recursion is `transparent') was
> believed to be undecidable.

It IS a difficult problem, but there is actually a hope.  Solomon
proved in '78 that the equivalence problem between a limited form of
parametric types reduces to the equivalence between deterministic
pushdown automata.  The latter had been a long-standing big problem.
Very recently ('97), it was solved: decidable.  If you are interested,
look into these papers.

@InProceedings{Solomon78,
  author =       "Marvin Solomon",
  title =        "Type Definitions with Parameters",
  booktitle =    "Conference Record of the Fifth Annual {ACM} Symposium
                 on Principles of Programming Languages",
  address =      "Tucson, Arizona",
  organization = "ACM SIGACT-SIGPLAN",
  month =        jan # " 23--25,",
  year =         "1978",
  pages =        "31--38",
  note =         "Extended abstract",
}

@InProceedings{Senizergues97,
  author = 	 "G{\'{e}}raud S{\'{e}}nizergues",
  title = 	 "Decidability of the equivalence problem for
		  deterministic pushdown automata", 
  OPTcrossref =  "",
  OPTkey = 	 "",
  OPTeditor = 	 "",
  OPTvolume = 	 "",
  OPTnumber = 	 "",
  OPTseries = 	 "",
  OPTpages = 	 "",
  booktitle =	 "Proceedings of INFINITY'97",
  year =	 "1997",
  OPTorganization = "",
  OPTpublisher = "",
  OPTaddress = 	 "",
  OPTmonth = 	 "",
  OPTnote = 	 "",
  OPTannote = 	 ""
}

Hope helps,

Haruo
-------------------
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] How to compare recursive types?

[John Max Skaller]

Andreas Rossberg wrote:

>This is highly off-topic, but anyway...
>
Aw, come on. I'm writing a compiler using Ocaml.
Who else would I ask about a typing problem than people
who regularly use ocaml to implement compilers?
I don't read news, I subscribe to exactly one mailing list (this one)
and I'm neither an academic or a student.

>
>John Max Skaller wrote:
>
>>How to compare recursive types?
>>[Or more generally, datya structures ..]
>>
>>Here is my best solution so far.
>>For sake of argment types are either
>>
>>  a) primitive
>>  b) binary product
>>  c) typedef (alias) name
>>
>
>OK, so you don't have type lambdas (parameterised types).
>
Not yet no... they're next :-)

> In that case
>any type term can be interpreted as a rational tree. 
>
.. what's that?

>
>If you add lambdas (under recursion) things get MUCH harder. Last time I
>looked the problem of equivalence of such types under the equi-recursive
>interpretation you seem to imply (i.e. recursion is `transparent') was
>believed to be undecidable.
>
In the first instance, the client will have to apply type functions
to create types ..

>>We compare the type expressions structurally and recursively,
>>also passing a counter value:
>>
>>  cmp 99 e1 e2
>>
>>When we reach a typedef name,
>>we decrement the counter argument.
>>
>>If the counter drops
>>to zero, we return true, otherwise we
>>replace the name by the expression it denotes
>>and continue (using the decremented counter).
>>
>
>So you return true for any infinite (i.e. recursive) type.
>Interesting...
>
No of course not. Obviously, you return false if you reach
two different primitives, or a product and a primitive.

>
>Seriously, what do you mean by "reaching a typedef name"? In one
>argument? 
>
Yes. In one of the arguments.

>In both simultanously? What if you reach different names? 
>
No, and irrelevant given that.

>From
>the second paragraph it seems that you have only considered one special
>case. For the others, if your counter dropped to 0, you had to return
>false for the sake of termination, which renders the algorithm incorrect
>(or incomplete, if you want to put it mildly).
>
I don't understand: probably because my description of the algorithm
was incomplete, you didn't follow my intent. Real code below.

>>It is "obvious" that for a suitably large counter,
>>this algorithm always terminates and gives the
>>correct result. [The proof would follow from
>>some kind of structural induction]
>>
>
>I doubt that ;-) In fact it is obvious that your algorithm is incorrect.
>[The proof is a simple counter example like (cmp n t1 t2) where
>t1=prim*t1, t2=prim*t2.]
>
No, that case is handled easily. Output of code below:
-----------------------------------------------------
(((fix 1 * float) as 2 * int) as 1 * float)
((fix 1 * int) as 2 * float) as 1
equal
(fix 1 * int) as 1
(fix 1 * int) as 1
equal
-----------------------------------------------------

type node_t =
  | Prim of string
  | Pair of node_t * node_t
  | Name of string

type env_t = (string * node_t) list

type lnode_t =
  | LPrim of string
  | LPair of lnode_t * lnode_t
  | LBind of int * lnode_t
  | LFix of int

let rec bind' env n labels t = match t with
  | Prim s -> LPrim s
  | Pair (t1, t2) ->
    LPair
    (
      bind' env n labels t1,
      bind' env n labels t2
    )
  | Name s ->
    if List.mem_assoc s labels
    then LFix (List.assoc s labels)
    else
      LBind
      (
        n,
        bind' env (n+1) ((s,n)::labels) (List.assoc s env)
      )

let bind env t =  bind' env 1 [] t

let rec str t = match t with
  | LPrim s -> s
  | LPair (t1,t2) -> "(" ^ str t1 ^ " * " ^ str t2 ^ ")"
  | LBind (i,t) -> str t ^ " as " ^ string_of_int i
  | LFix i -> "fix " ^ string_of_int i


let rec cmp n lenv renv x y =
  if n = 0 then true
  else match x, y with
  | LPrim s, LPrim r -> s = r
  | LPair (a1,a2), LPair (b1,b2) ->
    cmp n lenv renv a1 b1 &&
    cmp n lenv renv a2 b2
  | LBind (i,a),_ ->
    cmp n ((i,a)::lenv) renv a y
  | _, LBind (i,b) ->
    cmp n lenv ((i,b)::renv) x b
  | LFix i,_ ->
    cmp (n-1) lenv renv (List.assoc i lenv) y
  | _,LFix i ->
    cmp (n-1) lenv renv x (List.assoc i renv)
  |  _ -> false
 
let env = [
  "x", Pair (Name "y", Prim "int");  (* typedef x = y * int *)
  "y", Pair (Name "x", Prim "float") (* typedef y = x * float *)
]

(* t1 = x * float, this equals y *)
let t1 = Pair (Name "x", Prim "float")
let t1' = bind env t1
let t2' = bind env (Name "y")
;;

print_endline (str t1');;
print_endline (str t2');;

print_endline
(
  match cmp 10 [] [] t1' t2' with
  | true -> "equal"
  | false -> "not equal"
)
;;

let env = [
  "x", Pair (Name "x", Prim "int");
  "y", Pair (Name "y", Prim "int")
]
;;

let t1 = bind env (Name "x")
let t2 = bind env (Name "y")
;;

print_endline (str t1);;
print_endline (str t2);;

print_endline
(
  match cmp 10 [] [] t1 t2 with
  | true -> "equal"
  | false -> "not equal"
)
;;



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

Re: [Caml-list] How to compare recursive types?

[Andreas Rossberg]

John Max Skaller wrote:
> 
> > In that case
> >any type term can be interpreted as a rational tree.
> >
> .. what's that?

An infinite tree that has only a finite number of different subtrees.
Such trees can naturally be represented as cyclic graphs.

> >If you add lambdas (under recursion) things get MUCH harder. Last time I
> >looked the problem of equivalence of such types under the equi-recursive
> >interpretation you seem to imply (i.e. recursion is `transparent') was
> >believed to be undecidable.
> >
> In the first instance, the client will have to apply type functions
> to create types ..

I don't understand what you mean. If you have type functions you have
type lambdas, even if they are implicit in the source syntax. And
decidability of structural recursion between type functions is an open
problem, at least for arbitrary functions, so be careful. (Thanks to
Haruo for reminding me of Salomon's paper, I already forgot about that.)

OCaml avoids the problem by requiring uniform recursion for structural
types, so that all lambdas can be lifted out of the recursion.

> >[...]
> 
> I don't understand: probably because my description of the algorithm
> was incomplete, you didn't follow my intent. Real code below.

OK, now it is getting clearer. Your idea is to unroll the types k times
for some k. Of course, this is trivially correct for infinite k. The
correctness of your algorithm depends on the existence of a finite k.

> I guess that, for example, 2(n +1) is enough for the counter,
> where n is the number of typedefs in the environment.

I don't think so. Consider:

	t1 = a*(a*(a*(a*(a*(a*(a*(a*b)))))))
	t2 = a*t2

This suggests that k must be at least 2m(n+1), where m is the size of
the largest type in the environment. Modulo this correction, you might
be correct.

Still, ordinary graph traversal seems the more appropriate approach to
me: represent types as cyclic graphs and check whether the reachable
subgraphs are equivalent.

There is also a recent paper about how to apply hash-consing techniques
to cyclic structures:

@article{Mauborgne:IncrementalUniqueRepresentation,
  author	= "Laurent Mauborgne",
  title		= "An Incremental Unique Representation for Regular Trees",
  editor	= "Gert Smolka",
  journal	= "Nordic Journal of Computing",
  volume	= 7,
  pages		= "290--311",
  year		= 2000,
  month		= nov,
}

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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] How to compare recursive types?

[John Max Skaller]

Andreas Rossberg wrote:

>John Max Skaller wrote:
>
>>>In that case
>>>any type term can be interpreted as a rational tree.
>>>
>>.. what's that?
>>
>
>An infinite tree that has only a finite number of different subtrees.
>Such trees can naturally be represented as cyclic graphs.
>
Ah, thanks.

>>>If you add lambdas (under recursion) things get MUCH harder. Last time I
>>>looked the problem of equivalence of such types under the equi-recursive
>>>interpretation you seem to imply (i.e. recursion is `transparent') was
>>>believed to be undecidable.
>>>
>>In the first instance, the client will have to apply type functions
>>to create types ..
>>
>
>I don't understand what you mean. 
>
Like C++ tempates.

    all (x:type) type list = Empty | x * list x;
    all (x:type) fun rev(a:list x): list x = { .. code to reverse a list }

but the only way to use it will be to instantiate it manually to create
an actual type:

  val x:list int = ....
  val y:list int = rev[int] x;

so the compiler doesn't have to deal directly with the type functions,
other than to apply them to create instance types.

>If you have type functions you have
>type lambdas, even if they are implicit in the source syntax. And
>decidability of structural recursion between type functions is an open
>problem, at least for arbitrary functions, so be careful. (Thanks to
>Haruo for reminding me of Salomon's paper, I already forgot about that.)
>
>OCaml avoids the problem by requiring uniform recursion for structural
>types, so that all lambdas can be lifted out of the recursion.
>
Ah. I see... you don't happen to have any references to online
material explaining that? .. let me guess, the fixpoints aren't allowed
inside the lambdas .. ok .. I have a picture of it in my head ..

>>>[...]
>>>
>>I don't understand: probably because my description of the algorithm
>>was incomplete, you didn't follow my intent. Real code below.
>>
>
>OK, now it is getting clearer. Your idea is to unroll the types k times
>for some k. Of course, this is trivially correct for infinite k. The
>correctness of your algorithm depends on the existence of a finite k.
>
Yes. And I contend it must exist, for a rational tree: the problem is
calculating it... or finding a better algorithm.

>>I guess that, for example, 2(n +1) is enough for the counter,
>>where n is the number of typedefs in the environment.
>>
>
>I don't think so. Consider:
>
>	t1 = a*(a*(a*(a*(a*(a*(a*(a*b)))))))
>	t2 = a*t2
>
You are right, I thought of this example myself.

>
>This suggests that k must be at least 2m(n+1), where m is the size of
>the largest type in the environment. Modulo this correction, you might
>be correct.
>
Yes, that seems like a good starting point.. though that number is
VERY large .. the 'unrolling' is exponential .. so my algorithm
is not very good: k is global .. so many unrollings are too long ..

>
>Still, ordinary graph traversal seems the more appropriate approach to
>me: represent types as cyclic graphs and check whether the reachable
>subgraphs are equivalent.
>
Yeah .. well .. that's what my algorithm is doing ..
I just need a better algorithm  :-)

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

Re: [Caml-list] How to compare recursive types?

[John Max Skaller]

Argg.. my algorithm is wrong. Here is a counterexample:

typedef x = x * int;
typedef y = (y * int) * int;

If you just unroll these types for a while, they look equal,
but they aren't: in fact y might be considered a subtype of x.
Type x is any cyclic list of n>0 ints.
Type y is any non-empty cyclic list of an *even* number of ints.
Y might be represented in C using

struct y {
  y *next;
  int first;
  int second;
};

Now I *really* need a proper algorithm ..

Felix is extensional: in a product, we normally expand
types, but we can't do that if the type is recursive.

A pointer must be used not only at the fix point,
but at any possible fixpoint of an equivalent
definition...so any strongly connected components
have to be refered to by a pointer I think .. this
would solve the representation problem above
(at least in this case) but the fact remains
that the types above are not equal.

A similar example:

x2 = x * int;
x3 = x2 * int;
...

shows how to construct a type holding 'at least'
a certain number of ints... and my algorithm
also fails to distinguish these types.
Here., the representations would be different ..
there is no recursion in the 'top' part of the type,
so an expanded struct would be used ..

Hmmm.. does it show one type is a subtype
of the other .. hmmm .. perhaps it shows that
there exists a type  which both types are
subtypes of .. that sounds right ..


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

Re: [Caml-list] How to compare recursive types? Solution!

[John Max Skaller]

OK, I think I have a solution .. and it is so dang simple too.

Basically, I normalise the type terms and use ocamls polymorphic
equality operator! The normalisation involves counting what
*real* level of the tree the recursive descent is in -- add one for
each binary Pair node. Each typedef name substituted along
the branch is tracked in an association list along with its level.
When a typedef name is encountered that is in this list,
replace it with Fix n, where n is the associated level number:
this uniquely determines the recursion argument.

The result of this algorithm is completely different to
what I had before .. and it seems right. There's ONLY
one way to represent a given type here.

The intended model is: a pair is a C struct,
the included types are expanded if they're
not strongly coupled with the containing type
if they are, a pointer is used.
[I think this model is sound, I'm not sure yet ..]

----------------------------------------------------------------------
type node_t =
  | Prim of string
  | Pair of node_t * node_t
  | Name of string

type env_t = (string * node_t) list

type lnode_t =
  | LPrim of string
  | LPair of lnode_t * lnode_t
  | LFix of int

let rec bind' env n labels t = match t with
  | Prim s -> LPrim s
  | Pair (t1, t2) ->
    LPair
    (
      bind' env (n+1) labels t1,
      bind' env (n+1) labels t2
    )
  | Name s ->
    if List.mem_assoc s labels
    then LFix (List.assoc s labels)
    else
      bind' env n ((s,n)::labels) (List.assoc s env)

let bind env t =  bind' env 0 [] t


let rec str' n t =
  string_of_int n ^":" ^
  match t with
  | LPrim s -> s
  | LPair (t1,t2) -> "(" ^ str' (n+1) t1 ^ " * " ^ str' (n+1) t2 ^ ")"
  | LFix i -> "fix " ^ string_of_int i

let str t = str' 0 t

let cmp a b = a = b
let strb b = if b then "true" else "false"
let pres a b =
  print_endline (str a);
  print_endline (str b);
  let res = cmp a b in
  print_endline (strb res)
;;

(* ---------------------------------- *)
let env = [
  "x", Pair (Name "y", Prim "int");  (* typedef x = y * int *)
  "y", Pair (Name "x", Prim "float") (* typedef y = x * float *)
]

let t1 = Pair (Name "x", Prim "float")
let t1' = bind env t1
let t2' = bind env (Name "y")
;;

pres t1' t2';; (* FALSE *)

(* ---------------------------------- *)
let env = [
  "x", Pair (Name "x", Prim "int");
  "y", Pair (Name "y", Prim "int")
]
;;

let t1' = bind env (Name "x")
let t2' = bind env (Name "y")
;;

pres t1' t2';; (* TRUE *)

(* ---------------------------------- *)
let env = [
  "x", Pair (Pair (Name "x", Prim "int"), Prim "int");
  "y", Pair (Name "y", Prim "int")
]
;;

let t1' = bind env (Name "x")
let t2' = bind env (Name "y")
;;

pres t1' t2';; (* FALSE *)

(* ---------------------------------- *)

pres t1' t1';; (* TRUE *)

(* ---------------------------------- *)
let env = ["x", Name "x"]
let t = bind env (Name "x")
;;
pres t t;;

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

Re: [Caml-list] How to compare recursive types?

[Andreas Rossberg]

John Max Skaller wrote:
> 
> >>>If you add lambdas (under recursion) things get MUCH harder. Last time I
> >>>looked the problem of equivalence of such types under the equi-recursive
> >>>interpretation you seem to imply (i.e. recursion is `transparent') was
> >>>believed to be undecidable.
> >>>
> >>In the first instance, the client will have to apply type functions
> >>to create types ..
> >
> >I don't understand what you mean.
> 
> Like C++ tempates.
> 
>     all (x:type) type list = Empty | x * list x;

But that's not the point. You do the same in ML. Still, if you allow
arbitrary (probably higher-order) type declarations of the above form to
be mutually recursive, it is unknown whether you can still decide type
equivalence.

> so the compiler doesn't have to deal directly with the type functions,
> other than to apply them to create instance types.

It has, because reduction of an application of a recursive type function
may yield new redexes. In general, this procedure does not terminate.
Using non-uniform recursion you can create type terms that correspond to
irrational trees.

> >OCaml avoids the problem by requiring uniform recursion for structural
> >types, so that all lambdas can be lifted out of the recursion.
>
> Ah. I see... you don't happen to have any references to online
> material explaining that?

Not really, but the OCaml sources are relatively readable :-)

> .. let me guess, the fixpoints aren't allowed
> inside the lambdas .. ok .. I have a picture of it in my head ..

Not sure what you call "the fixpoints" (in your sources you called the
actual fixpoint construct "Bind" and used "Fix" for recursive refs).

Using the correct terminology the restriction is that lambdas are not
allowed under fixpoints.

> >Still, ordinary graph traversal seems the more appropriate approach to
> >me: represent types as cyclic graphs and check whether the reachable
> >subgraphs are equivalent.
> >
> Yeah .. well .. that's what my algorithm is doing ..
> I just need a better algorithm  :-)

Why not use standard graph algorithms then?

> Argg.. my algorithm is wrong. Here is a counterexample:
> 
> typedef x = x * int;
> typedef y = (y * int) * int;
> 
> If you just unroll these types for a while, they look equal,
> but they aren't: in fact y might be considered a subtype of x.
> Type x is any cyclic list of n>0 ints.
> Type y is any non-empty cyclic list of an *even* number of ints.

Huh? These types ARE equal: they both have the same infinite unrolling.
The rational trees representing them are equal in the theories I know of
- speaking of even or odd does not make any sense for infinite counts.

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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] How to compare recursive types?

[Jerome Vouillon]

On Wed, Apr 24, 2002 at 04:55:29PM +1000, John Max Skaller wrote:
> How to compare recursive types?

You should definitively read "Recursive Subtyping Revealed" by
Vladimir Gapeyev, Michael Levin, and Benjamin Pierce.
(Available from http://www.cis.upenn.edu/~bcpierce/papers/index.html)

If you are only interested in equality, you can use the same algorithm
as for subtyping (equality is a preorder).  The complexity of this
algorithm can be improved from quadratic to (almost) linear by
exploiting the fact that type equality is an equivalence relation: the
algorithm uses a set of pairs of already encountered types, but you
can use a union-find datastructure instead.

-- Jerome
-------------------
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] How to compare recursive types? Solution!

[Jerome Vouillon]

On Thu, Apr 25, 2002 at 05:03:12PM +1000, John Max Skaller wrote:
> Basically, I normalise the type terms and use ocamls polymorphic
> equality operator! The normalisation involves counting what
> *real* level of the tree the recursive descent is in -- add one for
> each binary Pair node. Each typedef name substituted along
> the branch is tracked in an association list along with its level.
> When a typedef name is encountered that is in this list,
> replace it with Fix n, where n is the associated level number:
> this uniquely determines the recursion argument.

Assume the following definition:
  typedef y = int * y;
Then "y" and "int * y" are not equal according to your algorithm.
Is it what you expect?

Why don't you make the pointers explicit in the type?  Then, the two
types definitions below would not define the same type
  typedef x = ref(x) * int;
  typedef y = (ref(y) * int) * int;
while these two would define the same type
  typedef x = ref(x) * int;
  typedef y = ref(ref(y) * int) * int;

-- Jerome
-------------------
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] How to compare recursive types?

[John Max Skaller]

Jerome Vouillon wrote:

>On Wed, Apr 24, 2002 at 04:55:29PM +1000, John Max Skaller wrote:
>
>>How to compare recursive types?
>>
>
>You should definitively read "Recursive Subtyping Revealed" by
>Vladimir Gapeyev, Michael Levin, and Benjamin Pierce.
>(Available from http://www.cis.upenn.edu/~bcpierce/papers/index.html)
>
>If you are only interested in equality, 
>
Actually, with my definition of equality I can just compare
terms. But then I am still left with a requirement to establish
if A is a subtype of B.

Thanks for info.. I'll check out the papers. Good to see stuff online.
(because that's all I have access to :-)

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

Re: [Caml-list] How to compare recursive types? Solution!

[John Max Skaller]

Jerome Vouillon wrote:

>
>Assume the following definition:
>  typedef y = int * y;
>Then "y" and "int * y" are not equal according to your algorithm.
>Is it what you expect?
>
It's what I expect from the algorithm, yes: the interpretation
would be a pair whose first component contains a y which
will be cyclic .. however none of the pointers in that cycle
point to the top level pair. Its a dubious distinction though ..
clearly I need to know that int * y is a subtype of y ..

>
>Why don't you make the pointers explicit in the type?  
>
The language does have pointers. I could ban type recursion
that does not go through a pointer, and that would make
sense (it is what C does). However, I allow unions like:

    union list = Empty |  Cons of int * list

where you can just write "list" instead of having
to specify a pointer .. part of the reason is that the
underlying implementation always uses a pointer
for constructor arguments, a single C type

  struct { int variant; void *data; }

is used for variant components. Now I am trying
to generalise that, to get rid of what might appear
as an inconsistency .. direct recursion is allowed
in one place but not another.

>Then, the two
>types definitions below would not define the same type
>  typedef x = ref(x) * int;
>  typedef y = (ref(y) * int) * int;
>while these two would define the same type
>  typedef x = ref(x) * int;
>  typedef y = ref(ref(y) * int) * int;
>
Yes .. but what would I do for the list?

To make matters worse, my pointers always
allow writing .. i'd have to adopt a second
kind that didn't like 'ref' .. the experience in
C/C++ with 'const' suggests it might be worth
trying to avoid this . . so I'm trying to use the
approach languages like ocaml use where the use of pointers is hidden ..
at the same time, I support overloading,
and expand types in structs (products)  to reduce the
cost of dereferencing and garbage collection.

Perhaps what I am trying to do is impossible.

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