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

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?

[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

Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 568 bytes --]

I have a question... I hope it will not be dismissed right away, thou I
guess most of you will find it stupid (some might however agree with me...
hopefully).

Cut the crap!

So... why actually are polymorphic variants useful? Why can't they simply be
implemented as normal, concrete (or how would you call them? ...) variants?
Doesn't the use of polymorphic variants just mess up the function type?

I'm not orthogonally against polymorphic variants, it's just that I am
looking for an alternative concept that could be used instead... Maybe
subtyped records?

- Tom

[-- Attachment #2: Type: text/html, Size: 614 bytes --]

Re: [Caml-list] Polymorphic Variants

[Seth J. Fogarty]

I find them prinicipally useful in three situations:

1) When I am writing code for an easy subset of a problem, and wish to
extend it later. This is the least useful case, easiest to replace.

2) When I have different overlapping kinds of data, with a common root
and common parent, and functions that are only defined on certain
branches of the 'type tree.' This would be the hardest to replicate.

3) When I have intermediate labelled data for gathering different
subproblems together. This is the neatest use: I extend my algorithm
to handle a case that might return the top two, and I just add an
additional case to the destructor for `TopTwo instead of `Best or
`SecondBest.

On 1/16/07, Tom <tom.primozic@gmail.com> wrote:
> I have a question... I hope it will not be dismissed right away, thou I
> guess most of you will find it stupid (some might however agree with me...
> hopefully).
>
> Cut the crap!
>
> So... why actually are polymorphic variants useful? Why can't they simply be
> implemented as normal, concrete (or how would you call them? ...) variants?
> Doesn't the use of polymorphic variants just mess up the function type?
>
> I'm not orthogonally against polymorphic variants, it's just that I am
> looking for an alternative concept that could be used instead... Maybe
> subtyped records?
>
> - Tom
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list:
> http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>
>


-- 
Seth Fogarty             sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large    AIM: Sorrath
"Let us not seek to satisfy our thirst for freedom by drinking from
the cup of bitterness and hatred." - Martin Luther King, Jr.

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 840 bytes --]

On 16/01/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
>
>
> 2) When I have different overlapping kinds of data, with a common root
> and common parent, and functions that are only defined on certain
> branches of the 'type tree.' This would be the hardest to replicate.
>

Could this be replicated by either
using overloaded non-polymorphic variants, meaning that say Int of int can
be shared by many types (almost like polymorphic variants, just that it is
declared, and thus (at least I believe so) more typesafe)

using records with overloaded fields and subtyping, so that you could have:
type top = {common of string}
type one_level_deep = {top | my_only of int}

type independent = {my_only of string}
so this would be possible:
let to_str x -> x.common

to_str {common = "first"}; to_str {common = "second"; my_only = 0}
?

- Tom

[-- Attachment #2: Type: text/html, Size: 1425 bytes --]

Re: [Caml-list] Polymorphic Variants

[Seth J. Fogarty]

On 1/16/07, Tom <tom.primozic@gmail.com> wrote:
>
>
> On 16/01/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
> >
> > 2) When I have different overlapping kinds of data, with a common root
> > and common parent, and functions that are only defined on certain
> > branches of the 'type tree.' This would be the hardest to replicate.
> >
>
> Could this be replicated by either
> using overloaded non-polymorphic variants, meaning that say Int of int can
> be shared by many types (almost like polymorphic variants, just that it is
> declared, and thus (at least I believe so) more typesafe)

Are you going to allow translation between these? Rho-variable
polymorphism is 'The Right Thing To Do' in this case with minimal type
annotation.

> using records with overloaded fields and subtyping, so that you could have:
> type top = {common of string}
> type one_level_deep = {top | my_only of int}
>
> type independent = {my_only of string}
> so this would be possible:
> let to_str x -> x.common
>
> to_str {common = "first"}; to_str {common = "second"; my_only = 0}
> ?

OCaml does not, as far as I know, have any structural typing for
records.. and I am not sure this would be at all cleaner. It might
WORK, but it would be just as ugly, if not uglier.


-- 
Seth Fogarty             sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large    AIM: Sorrath
"Let us not seek to satisfy our thirst for freedom by drinking from
the cup of bitterness and hatred." - Martin Luther King, Jr.

Re: [Caml-list] Polymorphic Variants

[Edgar Friendly]

Seth J. Fogarty wrote:
>> using records with overloaded fields and subtyping, so that you could
>> have:
>> type top = {common of string}
>> type one_level_deep = {top | my_only of int}
>>
>> type independent = {my_only of string}
>> so this would be possible:
>> let to_str x -> x.common
>>
>> to_str {common = "first"}; to_str {common = "second"; my_only = 0}
>> ?
> 
> OCaml does not, as far as I know, have any structural typing for
> records.. and I am not sure this would be at all cleaner. It might
> WORK, but it would be just as ugly, if not uglier.
> 
> 
OCaml's records are tuples with named accessors to the components.
Within a namespace, these accessors must be unique, so the type
independent wouldn't be possible, because the my_only component wouldn't
always be in the same position.

E.

Re: [Caml-list] Polymorphic Variants

[Lukasz Stafiniak]

On 1/16/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
> On 1/16/07, Tom <tom.primozic@gmail.com> wrote:
> >
> >
> > On 16/01/07, Seth J. Fogarty <sfogarty@gmail.com> wrote:
...
> > using records with overloaded fields and subtyping, so that you could have:
> > type top = {common of string}
> > type one_level_deep = {top | my_only of int}
> >
> > type independent = {my_only of string}
> > so this would be possible:
> > let to_str x -> x.common
> >
> > to_str {common = "first"}; to_str {common = "second"; my_only = 0}
> > ?
>
> OCaml does not, as far as I know, have any structural typing for
> records.. and I am not sure this would be at all cleaner. It might
> WORK, but it would be just as ugly, if not uglier.
>
OCaml has objects, which is a heavy-weight solution to the "structural
subtyping for records" problem. Polymorphic variants make one wonder,
if such light-weight solution could exist for records also, and you
conjecture, that it doesn't. What is the minimal nice version of
structural subtyping for records? Is it objects without classes and
field / method separation (but with late binding)?

Re: [Caml-list] Polymorphic Variants

[skaller]

On Tue, 2007-01-16 at 15:23 -0600, Seth J. Fogarty wrote:

> OCaml does not, as far as I know, have any structural typing for
> records.. 

Hmm .. Felix does, and it supports subtyping (by explicit coercion).
So why doesn't Ocaml have it? Yes, it would be "yet another product
type", bringing the total to 4 in Ocaml (tuples, records, structurally
typed records and classes).

Come to think of it .. aren't classes structurally typed records?


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

Re: [Caml-list] Polymorphic Variants

[Jonathan Roewen]

There are interesting, and extremely useful use cases for polymorphic
variants. One very cool example (IMO) is an xhtml module which mixes
phantom types with polymorphic variants so that the compiler enforces
creation of valid xhtml documents (with some limitations...).

Also, OCaml has ways to control whether a polymorphic variant argument
to a function is open/extensible or not.

As for the records issue: you can wrap them in sub modules to
workaround the name clash problem by fully qualifying the fields with
their module name.

E.g.

module A = struct
  type t = { x : int; y : int }
end

module B = struct
  type t = { x : float; y : float }
end

open A;;
open B;;

let a = { A.x = 2; A.y = 3 };;
let b = { B.x = 1.; B.y = 2. };;

let x_from_A v = v.A.x;;
let x_from_B v = v.B.x;;

Jonathan

On 1/17/07, Tom <tom.primozic@gmail.com> wrote:
> I have a question... I hope it will not be dismissed right away, thou I
> guess most of you will find it stupid (some might however agree with me...
> hopefully).
>
> Cut the crap!
>
> So... why actually are polymorphic variants useful? Why can't they simply be
> implemented as normal, concrete (or how would you call them? ...) variants?
> Doesn't the use of polymorphic variants just mess up the function type?
>
> I'm not orthogonally against polymorphic variants, it's just that I am
> looking for an alternative concept that could be used instead... Maybe
> subtyped records?
>
> - Tom
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list:
> http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>
>

Re: [Caml-list] Polymorphic Variants

[Jacques GARRIGUE]

From: Tom <tom.primozic@gmail.com>
> So... why actually are polymorphic variants useful? Why can't they simply be
> implemented as normal, concrete (or how would you call them? ...) variants?

The original motivation was for the LablTk library, where some types
(index for instance) have lots of small variations. At that point
there where several options
* overloading (but ocaml loathes overloading, you could say that the
  total absence of overloading is essential to the language)
* refinement types: define a type with all constructors, and have
  restricted versions of it where only some constructors are allowed
* full polymorphism, i.e. polymorphic variants

If you eliminate the first option, then the choice is between
refinement types and polymorphic variants. Refinement types are rather
attractive: they combine precise typing with explicit declarations.
The arguments in favour of polymorphic variants are
* they were somehow easier to add, as they are an orthogonal extension
  of the type system
* one can add new cases afterwards.
* they are defined structurally: two identical definitions in two
  different modules are equivalent. This can be pretty handy at times.
* you don't need to open a module to use them: mixes nicely with ocaml
  programming style

>From modularity considerations, it ends up being nicer to write
     type t = [`A of int |`B of bool]
     type u = [t | `C of char]
than
     type u = A of int | B of bool | C of char
     type t = u[A B]

Afterwards I discovered that, using some idioms, they also allow
extensible programs in a very concise way. (Much more concise than
objects, when they are relevant.)

> Doesn't the use of polymorphic variants just mess up the function type?
What do you mean by "mess up the function type"?
If you mean that, without type annotations, types and errors become
very hard to read, this is true, but the manual explicitely encourages
to add type annotations :-)

> I'm not orthogonally against polymorphic variants, it's just that I am
> looking for an alternative concept that could be used instead... Maybe
> subtyped records?

In terms of expressiveness, you can simulate polymorphic variants
using objects (which are subtyped records,) but this is often much
more verbose, and requires higher order types. I have some code using
objects (visitor pattern), recursive modules, lazyness, and private
row types, in an utterly non trivial way, just to do what can be done
by standard recursive function definitions using polymorphic variants...

Jacques Garrigue

Re: [Caml-list] Polymorphic Variants

[Christophe TROESTLER]

On Wed, 17 Jan 2007, Jacques GARRIGUE <garrigue@math.nagoya-u.ac.jp> wrote:
> 
> [...] I have some code using objects (visitor pattern), recursive
> modules, lazyness, and private row types, in an utterly non trivial
> way, just to do what can be done by standard recursive function
> definitions using polymorphic variants...

Sounds like a good case to see & learn the power of polymorphic
variants in action.  Are the two codes available somewhere (if
possible with some explanations ?) or are you simply referring to your
paper "Code reuse through polymorphic variants" ?

Regards,
ChriS

Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue]

From: Christophe TROESTLER <Christophe.Troestler+ocaml@umh.ac.be>
> > [...] I have some code using objects (visitor pattern), recursive
> > modules, lazyness, and private row types, in an utterly non trivial
> > way, just to do what can be done by standard recursive function
> > definitions using polymorphic variants...
> 
> Sounds like a good case to see & learn the power of polymorphic
> variants in action.  Are the two codes available somewhere (if
> possible with some explanations ?) or are you simply referring to your
> paper "Code reuse through polymorphic variants" ?

Well, I am. Other examples end up being much longer, even using
polymorphic variants :-)

But still, I include at the end of this mail the code to obtain a
fully extensible purely functional polymorphic visitor pattern.
(This is the polymorphic part that is particularly hard, even more
if you want to stay purely functional.)

For comparison, here is the equivalent complete code using polymorphic
variants. Note that there is no explicit visitor pattern: the match
construct provides it, with all the polymorphism needed.

type 'a eadd = [ `Num of int | `Add of 'a * 'a ]
let eval_add eval_rec : 'a eadd -> int = function
  | `Num i -> i
  | `Add (e1, e2) -> eval_rec e1 + eval_rec e2
let rec eval_add' e = eval_add eval_add' e
(* val eval_add' : ('a eadd as 'a) -> int *)
type 'a eaddneg = ['a eadd | `Neg of 'a]
let eval_add_neg eval_rec : 'a eaddneg -> int = function
  | #eadd as e -> eval_add eval_rec e
  | `Neg e -> - eval_rec e
let rec eval_add_neg' e = eval_add_neg eval_add_neg' e
(* val eval_add_neg' : ('a eaddneg as 'a) -> int *)
let n = eval_add_neg' (`Add (`Neg(`Add(`Num 3, `Num 2)), `Num 7))
(* val n : int = 2 *)

This also means that providing a method returning a polymorphic
variant describing the contents of an object is probably a simpler
approach to implementing the visitor pattern, even for objects. Here
is the code needed if you still want to use objects.

class type ['a] expr = object method repr : 'a end
let rec eval_add_expr (e : _ expr) = eval_add eval_add_expr e#repr
(* val eval_add_expr : ('a eadd expr as 'a) -> int *)
let rec eval_add_neg_expr (e : _ expr) = eval_add_neg eval_add_neg_expr e#repr
(* val eval_add_neg_expr : ('a eaddneg expr as 'a) -> int *)

Regards,

Jacques Garrigue

(* A fully extensible polymorphic visitor pattern.
   Code written with Keiko Nakata *)

class type ['a,'exp] visit_add = object
  method visitNum : int -> 'a
  method visitAdd : 'exp -> 'exp -> 'a
end

module type AddTE = sig
  type ('a,'exp) t
  type exp = < accept : 'a. ('a, exp) t -> 'a >
  val num : int -> exp
  val add : exp -> exp -> exp
end

module type AddT = sig
  include AddTE
  val eval : (int, exp) t Lazy.t
end

module AddF(X : AddT with type ('a,'exp) t = private ('a,'exp) #visit_add) =
struct
  type ('a, 'exp) t = ('a, 'exp) X.t
  class type exp = object ('e) method accept : 'a. ('a, 'e) t -> 'a end
  class num x = object (_ : #exp) method accept v = v#visitNum x end
  let num x = new num x
  class add a b = object (_ : #exp) method accept v = v#visitAdd a b end
  let add x = new add x
  class eval = object (eval)
    method private visit (e : exp) = e#accept (Lazy.force X.eval)
    method visitNum (i : int) = i
    method visitAdd r l = eval#visit r + eval#visit l
  end
  let eval = lazy (new eval)
end

module rec Add : AddT with type('a,'exp) t = ('a,'exp) visit_add = AddF(Add)

class type ['a,'exp] visit_add_neg = object
  inherit ['a,'exp] visit_add
  method visitNeg : 'exp -> 'a
end

module type AddNegT = sig
  include AddT
  val neg : exp -> exp
end

module AddNegF(X : AddNegT with
               type ('a,'exp) t = private ('a,'exp) #visit_add_neg) =
struct
  module Add = AddF(X)
  include (Add : AddTE with type ('a,'e) t = ('a,'e) X.t)
  class neg x = object (_ : #Add.exp) method accept v = v#visitNeg x end
  let neg x = new neg x
  class eval = object (eval)
    inherit Add.eval
    method visitNeg e = - eval#visit e
  end
  let eval = lazy (new eval)
end

module rec AddNeg : AddNegT with type ('a,'exp) t = ('a,'exp) visit_add_neg =
  AddNegF(AddNeg)

open AddNeg
let n = (add (neg (add (num 3) (num 2))) (num 7))#accept (Lazy.force eval)

Re: [Caml-list] Polymorphic Variants

[skaller]

On Wed, 2007-01-17 at 11:19 +0900, Jacques GARRIGUE wrote:

> If you mean that, without type annotations, types and errors become
> very hard to read, this is true, but the manual explicitely encourages
> to add type annotations :-)

You are not kidding .. and even type annotations don't always help.
I regularly get 100-200 line errors, even in cases where the compiler
clearly knows which tag is causing the problem.

But I would not give up the polymorphic variants despite this pain,
because the alternative is now unthinkable.

Basically, with ordinary variants if you have some subset
of cases you can handle it easily but verbosely with
morphisms:

	type X = | A | B | C | D
	type Y = | AA | BB

	let XtoY x : Y = match x with
	| A -> AA
	| B -> BB
	| _ -> failwith "blah"

	let YtoX y : X = match y with
	| AA -> A
	| BB -> B


With polymorphic variants these morphisms are created automatically,
and AFAIK the embedding (YtoX) has zero cost. You can also do:

	type X = [`A | `B | `C | `D]
	type Y = [`A | `B]

	let XtoY x: Y = match x with
	| #Y as y -> (y:X:>Y)
	| _ -> failwith "khg"


	let YtoX y: X = (y:Y:>X)

This is mainly "syntactic sugar". The recursive case is where 
polymorphic variants really shine, eg a compiler "expression"
type with various "sub expression" types where there are constraints
satisfied recursively by all nodes. (These things are still far too
hard to define with multiple parameters though .. ;(



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

Re: [Caml-list] Polymorphic Variants

[Andrej Bauer]

skaller wrote:

> You are not kidding .. and even type annotations don't always help.
> I regularly get 100-200 line errors, even in cases where the compiler
> clearly knows which tag is causing the problem.

Pah, that's nothing. An early version of Cduce ocassionally gave me 
error messages that were 1GB (!) in legnth. Now can your Felix do THAT?

Andrej

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 3329 bytes --]

On 17/01/07, Jacques GARRIGUE <garrigue@math.nagoya-u.ac.jp> wrote:
>
> From: Tom <tom.primozic@gmail.com>
> > So... why actually are polymorphic variants useful? Why can't they
> simply be
> > implemented as normal, concrete (or how would you call them? ...)
> variants?
>
> The original motivation was for the LablTk library, where some types
> (index for instance) have lots of small variations. At that point
> there where several options
> * overloading (but ocaml loathes overloading, you could say that the
>   total absence of overloading is essential to the language)
>

Is there a reason for that? Is it only hard to implement or are there any
conceptual / strategical / theoretical reasons?

> OCaml does not, as far as I know, have any structural typing for
> records..

Hm... Actually, what I had in mind is nominal subtyping... similar to
objects, in fact, objects in C++-like languages, just that they have no
class methods.

Now... close your eyes (but try to continue reading this ;) ) and imagine
you're in a dreamworld. You are programming in a language that has
  * function overloading that allows you to have
       length "abcd" + length [1; 2; 3]
  * Constructor overloading, eliminating the need of
       type parse_expression =
           Pexp_name of string
         | Pexp_constant of constant
         | Pexp_let of (pattern * parse_expression) * parse_expression
         | Pexp_apply of parse_expression * parse_expression list
         | Pexp_try of parse_expression * (pattern * parse_expression) list

       type typed_expression =
           Texp_ident of ident
         | Texp_constant of constant
         | Texp_let of (pattern * typed_expression) * typed_expression
         | Texp_apply of typed_expression * typed_expression list
         | Texp_try of typed_expression * (pattern * typed_expression) list
    as it can be coded as
       type parse_expression =
           Name of string
         | Constant of constant
         | ...

       type typed_expression =
           Ident of ident
         | Constant of constant
         | ...

  * nominal subtyping of records, with overloaded field names:
       type widget = {x : float; y : float; width: float; height: float} (*
top-level type *)
       type button = {widget | text : string }
       type checkbox = {button | checked : bool}
       type image = {widget | url : string}

       type vector = {x : float; y : float}
       type document {url : url}

    so subtypes could be applied to a function
       fun move : widget -> (float * float) -> unit

       let chk = {x = 0.0; y = 0.0; width = 10.0; height = 12.0; text =
"Check me!"; checked = false}
       move chk (3.0, 3.0)
    and types could be "discovered" at runtime:
       let draw widget =
         typematch widget with
             w : widget -> draw_box (w.x, w.y, w.height, w.width)
           | b : button -> draw_box (b.x, b.y, b.height, b.width); draw_text
b.text
           | i : image -> draw_image i.url (i.x, i.y)
           | ...

Do you think you would be "satisfied" even without polymorphic variants?

I am not saying this just for fun... I want to create a language with
overloading, but I kinda don't really like polymorphic variants... thou if
they turn out to be really useful, I would probably start to like them.

Any comments?

- Tom

[-- Attachment #2: Type: text/html, Size: 5258 bytes --]

Re: [Caml-list] Polymorphic Variants

[Jon Harrop]

On Wednesday 17 January 2007 21:13, Tom wrote:
> Any comments?

Yes: I prefer things the way they are.

You can add overloading to ML but you must then add lots of type annotations 
to your code. For example, vector length:

  let length (x, y) = sqrt(x*.x +. y*.y)

becomes:

  let length (x : float, y : float) = sqrt(x*x + y*y)

So you've saved the "." three times at the cost of ": float" twice because the 
overloaded * and + don't provide enough type information. You can complicate 
the type inferer to counteract this but then other type errors will become 
increasingly obscure and the programmer will be forced to learn the quirks 
that you've added in order to debug their code.

Constructor overloading can be done in OCaml using polymorphic variants. They 
are slower. Code written in this style quickly becomes unmaintainable because 
the type errors (from inference) are so complicated that you are forced to 
annotate types.

Finally, I don't want my types discovered at run-time because it makes my code 
slower and uses more memory. I'd rather have to box manually, so fast code is 
concise code.

From my point of view, your suggestions are mostly steps backwards (towards 
Lisp, C++ etc.).

I think the best way to improve OCaml is to write an IDE that sidesteps these 
problems, e.g. by typesetting the code "+." as "+".

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 1557 bytes --]

>
>
> Yes: I prefer things the way they are.


I don't mean an revolution. Rather a symbiosys.

You can add overloading to ML but you must then add lots of type annotations
> to your code. For example, vector length:
>
>   let length (x, y) = sqrt(x*.x +. y*.y)
>
> becomes:
>
>   let length (x : float, y : float) = sqrt(x*x + y*y)
>
> So you've saved the "." three times at the cost of ": float" twice because
> the
> overloaded * and + don't provide enough type information. You can
> complicate
> the type inferer to counteract this but then other type errors will become
> increasingly obscure and the programmer will be forced to learn the quirks
> that you've added in order to debug their code.


3 solutions:
  * sqrt has type of float -> float and the compiler infers float arguments
  * you write +. and *. (at least once) (those operators could be still
available, don't you think so?)
  * let the compiler overload your function ( length : (int * int) -> float;
length : (float * float) -> float) and then drop the "int" one as you never
ever used it in your code.


> Finally, I don't want my types discovered at run-time because it makes my
> code
> slower and uses more memory. I'd rather have to box manually, so fast code
> is
> concise code.


More memory is used by polymorphic variants too. And the records could be
optimised so that type information is only added when it is needed by the
programm.

>From my point of view, your suggestions are mostly steps backwards (towards
> Lisp, C++ etc.).


Thank you for your comment :)

- Tom

[-- Attachment #2: Type: text/html, Size: 2336 bytes --]

Re: [Caml-list] Polymorphic Variants

[Christophe TROESTLER]

On Wed, 17 Jan 2007, Jon Harrop <jon@ffconsultancy.com> wrote:
> 
> I think the best way to improve OCaml is to write an IDE that sidesteps these 
> problems, e.g. by typesetting the code "+." as "+".

Tuareg can do it.  Just put

  (setq tuareg-font-lock-symbols t)

in the appropriate section of your ~/.emacs

ChriS

Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue]

From: Tom <tom.primozic@gmail.com>
> On 17/01/07, Jacques GARRIGUE <garrigue@math.nagoya-u.ac.jp> wrote:
> > From: Tom <tom.primozic@gmail.com>
> > > So... why actually are polymorphic variants useful? Why can't they
> > simply be
> > > implemented as normal, concrete (or how would you call them? ...)
> > variants?
> >
> > The original motivation was for the LablTk library, where some types
> > (index for instance) have lots of small variations. At that point
> > there where several options
> > * overloading (but ocaml loathes overloading, you could say that the
> >   total absence of overloading is essential to the language)
> 
> Is there a reason for that? Is it only hard to implement or are there any
> conceptual / strategical / theoretical reasons?

There are two kinds of theoretical reasons.

The most theoretical one is about semantics: with generic overloading,
all your semantics must take types into account. This is a problem as
most theoretical studies of lambda-calculus are based on so-called
erasure semantics, where types are discarded at execution. So this
means you must design your own, more complex semantics. Not that this
reason may not apply to constructor or record overloading, if you do
not allow the semantics to change according to the type.

The other one is about type inference. Basically, overloading has a
huge impact on overloading. The direct way to handle it, using types
alone, is deeply disruptive, as it means that some programs will be
refused for lack of type information. It is very hard to define a
clear criterion on which programs should be refused, notwithstanding
internal details of the compiler. This also applies to record and
constructor overaloading. There are other approach the problem, with
constrained type variables (either Haskell's type classes or G'Caml's
generic type variables,) but of course they add complexity to the type
system. And it is not clear that they solve the problem for
constructor and record overloading: in Haskell, records fields are not
overloaded, and constructor overloading has to be done by hand for
each type, through an explicit encoding into type classes.

Both reasons have practical impact. For the first one, using erasure
semantics means that the programmer also can discard types when
understanding the runtime behaviour of a program. For the second one,
you can write code that is maximally polymorphic, without too much
fear about the impact of performance (equality is overloaded, so
it still matters...) or strange ambiguity-related error messages.

So for the time being ocaml keeps to no overloading at all.

> > OCaml does not, as far as I know, have any structural typing for
> > records..

Not for records, but for objects. From a type-theoretic point of view
they are just equivalent.

> Hm... Actually, what I had in mind is nominal subtyping... similar to
> objects, in fact, objects in C++-like languages, just that they have no
> class methods.

Reading the description below, this all looks nice, independently of
the semantics limitation described above. However, you can kiss
farewell to type inference. With such an extensive overloading, you
would need type annotations all over the place.
By the way, this all looks likes the "used this feature in C++"
syndrome. Sure C++ is incredibly powerful. But it is built on rather
shaky theoretical fundations. So you can't expect to bring everything
from C++ to a new language. Why not think about new ways to solve
problems :-)
(To be completely honest, this also looks a bit like ML2000, and the
Moby language, which has a sound theoretical fundation, but never
really took off. You might want to go see for yourself.)

Jacques Garrigue
 
> Now... close your eyes (but try to continue reading this ;) ) and imagine
> you're in a dreamworld. You are programming in a language that has
>   * function overloading that allows you to have
>        length "abcd" + length [1; 2; 3]
>   * Constructor overloading, eliminating the need of
>        type parse_expression =
>            Pexp_name of string
>          | Pexp_constant of constant
>          | Pexp_let of (pattern * parse_expression) * parse_expression
>          | Pexp_apply of parse_expression * parse_expression list
>          | Pexp_try of parse_expression * (pattern * parse_expression) list
> 
>        type typed_expression =
>            Texp_ident of ident
>          | Texp_constant of constant
>          | Texp_let of (pattern * typed_expression) * typed_expression
>          | Texp_apply of typed_expression * typed_expression list
>          | Texp_try of typed_expression * (pattern * typed_expression) list
>     as it can be coded as
>        type parse_expression =
>            Name of string
>          | Constant of constant
>          | ...
> 
>        type typed_expression =
>            Ident of ident
>          | Constant of constant
>          | ...
> 
>   * nominal subtyping of records, with overloaded field names:
>        type widget = {x : float; y : float; width: float; height: float} (*
> top-level type *)
>        type button = {widget | text : string }
>        type checkbox = {button | checked : bool}
>        type image = {widget | url : string}
> 
>        type vector = {x : float; y : float}
>        type document {url : url}
> 
>     so subtypes could be applied to a function
>        fun move : widget -> (float * float) -> unit
> 
>        let chk = {x = 0.0; y = 0.0; width = 10.0; height = 12.0; text =
> "Check me!"; checked = false}
>        move chk (3.0, 3.0)
>     and types could be "discovered" at runtime:
>        let draw widget =
>          typematch widget with
>              w : widget -> draw_box (w.x, w.y, w.height, w.width)
>            | b : button -> draw_box (b.x, b.y, b.height, b.width); draw_text
> b.text
>            | i : image -> draw_image i.url (i.x, i.y)
>            | ...
> 
> Do you think you would be "satisfied" even without polymorphic variants?
> 
> I am not saying this just for fun... I want to create a language with
> overloading, but I kinda don't really like polymorphic variants... thou if
> they turn out to be really useful, I would probably start to like them.
> 
> Any comments?
> 
> - Tom

Re: [Caml-list] Polymorphic Variants

[Jon Harrop]

On Thursday 18 January 2007 01:28, Jacques Garrigue wrote:
> ...ML2000...

What did happen to ML2000? Is it on a desert island with JPEG2000 and Fortran 
2000?

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] Polymorphic Variants

[skaller]

On Thu, 2007-01-18 at 10:28 +0900, Jacques Garrigue wrote:
> From: Tom <tom.primozic@gmail.com>

> > > * overloading (but ocaml loathes overloading, you could say that the
> > >   total absence of overloading is essential to the language)
> > 
> > Is there a reason for that? Is it only hard to implement or are there any
> > conceptual / strategical / theoretical reasons?
> 
> There are two kinds of theoretical reasons.
> 
> The most theoretical one is about semantics: with generic overloading,
> all your semantics must take types into account. This is a problem as
> most theoretical studies of lambda-calculus are based on so-called
> erasure semantics, where types are discarded at execution. 

Can you explain this more? The kind of overloading I'm used
to is a matter of lookup not semantics, i.e. its just syntactic
sugar to save the human reader's memory.

> Reading the description below, this all looks nice, independently of
> the semantics limitation described above. However, you can kiss
> farewell to type inference. With such an extensive overloading, you
> would need type annotations all over the place.

Felix makes this tradeoff. Types are deduced bottom up (s-attributes),
so variables and function return types are calculated, but function
parameters must be explicitly typed.

Even in Ocaml it is necessary to write some annotations
in two cases:

(a) hard to understand error messages from type inference

(b) polymorphic variants

On point (a) I admit I often *remove* the annotations
after writing them (which I can't do in Felix). The need
for (b) is limited and quite acceptable IMHO, it just takes
a bit more experience than I have to pick when you need
annotations or explicit coercions.

On the other hand some code would just be impossible
without overloading. For example C has

	char, short, int, long, long long
	unsigned versions
	float, double, long double

which is 13 distinct 'number' types, and I would hate
to have to write:

	1 int_add 2
	1L long_add 2L

Similarly I have had a 'pretty printer' program which prints
terms of an AST (the Felix grammar actually) and the fact I
could overload

	fun str : t -> string

meant I could usually forget what type it was I was converting
to a string. (There are something like 50 AST node types 
involved I think).

So in some cases with inference and without overloading,
*you need the annotations anyhow*, they just go into the
function names in an unprincipled manner, instead of going
into the function parameter types in a principled -- 
and indeed syntactically enforced -- manner.

Overall Felix library function declarations are considerably
more verbose than Ocaml .. but the implementation is about
the same complexity.

BTW: of course in Ocaml you can add annotations for documentation
purposes or to enforce a constraint.

> By the way, this all looks likes the "used this feature in C++"
> syndrome. 

Actually for Felix this is a legitimate reason :)

> Sure C++ is incredibly powerful. But it is built on rather
> shaky theoretical fundations.

What? C++ has theoretical foundations? 

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

Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue]

From: skaller <skaller@users.sourceforge.net>

> > The most theoretical one is about semantics: with generic overloading,
> > all your semantics must take types into account. This is a problem as
> > most theoretical studies of lambda-calculus are based on so-called
> > erasure semantics, where types are discarded at execution. 
> 
> Can you explain this more? The kind of overloading I'm used
> to is a matter of lookup not semantics, i.e. its just syntactic
> sugar to save the human reader's memory.

Because you're doing some partial evaluation :-)
Namely you can view an overloaded function as a function taking extra
hidden parameters: the types of its arguments. If these types are
monomorphic, then you can immediately partially evaluate your function
to choose the right implementation. But if they are polymorphic, you
need to pass extra information around. This is what is done in Haskell
for instance, passing dictionnaries for type classes.
So an alternative view is that overloading is a type dependent
translation from the source code to an explicit version. You can only
drop the types after this translation. So this means that you cannot
understand the source code locally: you need to be aware of the type
information around it.

> > Reading the description below, this all looks nice, independently of
> > the semantics limitation described above. However, you can kiss
> > farewell to type inference. With such an extensive overloading, you
> > would need type annotations all over the place.
> 
> Felix makes this tradeoff. Types are deduced bottom up (s-attributes),
> so variables and function return types are calculated, but function
> parameters must be explicitly typed.

This works if you don't add either subtyping or return-type
overloading to the mix. Then you must also know the type of variables
and the return type of functions. 

> Even in Ocaml it is necessary to write some annotations
> in two cases:
> 
> (a) hard to understand error messages from type inference
> 
> (b) polymorphic variants

This is not exactly the same thing, as these annotations have no
impact on the semantics. Of course, one could say: if we have the
annotation, why not use it for the semantics? But this is another
story, with different implications.

> On the other hand some code would just be impossible
> without overloading. For example C has
> 
> 	char, short, int, long, long long
> 	unsigned versions
> 	float, double, long double
> 
> which is 13 distinct 'number' types, and I would hate
> to have to write:
> 
> 	1 int_add 2
> 	1L long_add 2L

Actually this is not only overloading that is used here, but also
automatic conversions. When writing numeric computations in ocaml, I
find it just as painful to have to add float_of_int, as to add the dot
after all operators. (In number of characters, float_of_int might be
the biggest...)
For overloading alone, the module system could help.
If we had the operators defined with different types in each of the
numeric type modules, then one could just choose the numeric type used
with "open Mynumtype". This is one of the reasons I pushed for having
a local "let open" construct... which can be simulated by "let
module", at a slight cost.

> So in some cases with inference and without overloading,
> *you need the annotations anyhow*, they just go into the
> function names in an unprincipled manner, instead of going
> into the function parameter types in a principled -- 
> and indeed syntactically enforced -- manner.

I believe this is the strongest argument for overloading: that it
allows using types in a principled way. Of course, whether this is
really principled depends on the code you write...

Jacques Garrigue

Re: [Caml-list] Polymorphic Variants

[skaller]

On Thu, 2007-01-18 at 15:20 +0900, Jacques Garrigue wrote:
> From: skaller <skaller@users.sourceforge.net>

> > On the other hand some code would just be impossible
> > without overloading. For example C has
> > 
> > 	char, short, int, long, long long
> > 	unsigned versions
> > 	float, double, long double
> > 
> > which is 13 distinct 'number' types, and I would hate
> > to have to write:
> > 
> > 	1 int_add 2
> > 	1L long_add 2L
> 
> Actually this is not only overloading that is used here, but also
> automatic conversions.

In C/C++ yes, both overloading and automatic conversions.
In Felix there are no automatic conversions.

However Felix still allows you to write

	1 + 1L

if you open the module 'MixedInt'. That module provides
a constrained polymorphic function:

  fun add[t1:fast_ints, t2:fast_ints]: 
    t1 * t2 -> arithmax(t1,t2)
    ="$1+$2"
  ;

where 'fast_ints' is a typeset, which is a finite set
of concrete types, and 

	t: typeset

in this context means

	t where t isin typeset

(which is also legal Felix).

This is, in effect, the complete set of all the 100 overloads 
on the 10 C integer type pairs, represented as polymorphism 
with a constraint checked at the point of call. 

Note the implementation here is "$1+$2" which leverages
C++ overloading.

Typesets and constrained polymorphism are just a convenient
sugar for writing huge numbers of overloads out.

It is interesting that to model the C/C++ type system
here I had to do some quite advanced type system hackery,
but the result is mixed mode arithmetic without any
automatic conversions.

It is also possible to defer choice of types to the instantiation
phase, which can now be done in a well principled manner using
Felix typeclasses. In particular you can now, finally, after
6 years work, do a 'fold' on an STL container using typeclasses
without needing any 'dependent name lookup'.

this is not first class polyadic programming, since (unlike Haskell?)
only types can be typeclass parameters, not functors 
(type constructors, eg STL vector, list, set etc can't be arguments).

However the result is easier to use than Ocaml I think: 
typeclasses are weaker than Ocaml functors but they're much
easier to use, since they work with 'ordinary' code. 

In Ocaml to write 'generic' code you have to put your code 
inside a functor definition. Perhaps that is easy if you have,
for example, one container type, but typical programs will
use several container types, which would require several
levels of nested functors in Ocaml.

I think this would mean that the Ocaml code would be fragile
in the sense that you'd have to do a lot of housekeeping
if the implementation changed to use a slighly different
set of containers -- you'd have to rewrite all the
nested functor wrappers.

I wonder if there is a better way? I really don't like
typeclasses that much: they only allow a single instantiation.
For example

	1 < 2

is an instance of a total ordering typeclass for integers,
but integers can also be sorted in the other direction.
You can't have both orderings, instead you need a dummy
type

	type revint  = RevInt of int 

which supports the reverse ordering. Whereas with Ocaml/ML
functors the comparison function is a specific argument.
I think this is correct.

Hmm .. am I right in thinking Ocaml's local modules also allow
local functor instantiations? This must help quite a bit?

Having to explicitly instantiate is quite a pain though,
compared to C++ templates, typeclasses in either Haskell
or Felix, or plain old Ocaml polymorphic functions:
people keep asking for a polymorphic version of the 
Ocaml Set .. and I'm sure I use Hashtbl polymorphic version
to avoid having to instantiate Map all over the place ***

*** This is not so trivial due to lack of inter module
recursion across ml file boundaries

I wonder if Ocaml couldn't support automatic functor instantiation
by providing an "canonical" instance. For example:

module IntSet = Set.Make (Int)
module FloatSet = Set.Make (Float)

let s1 = IntSet.add s1 1            (* uses manual instantiation *)
let s2 = Set.Make(Int).add s 1      (* uses canonical instantiation *)

The canonical instantiation is 'generated' by the compiler.
It would have to be shared across ml files.

This would be similar to having nominally typed records BUT
also having a canonical structurally typed instance,
namely tuples.


>  When writing numeric computations in ocaml, I
> find it just as painful to have to add float_of_int, as to add the dot
> after all operators. (In number of characters, float_of_int might be
> the biggest...)

Nah, Felix uses BigInt internally for integers in case constants
fit in C integer types but not Ocaml ones .. BigInt.int_of_bigint
is bigger .. :)

> For overloading alone, the module system could help.
> If we had the operators defined with different types in each of the
> numeric type modules, then one could just choose the numeric type used
> with "open Mynumtype".

Yes. Interestingly in Felix you can open both modules
and typeclasses, AND you can partially specialise type
parameters if they're polymorphic, AND these things
can be overloaded .. all at once!

This can be a bit confusing .. especially since the typeclass
feature is new and undoubtedly contains bugs.

>  This is one of the reasons I pushed for having
> a local "let open" construct... which can be simulated by "let
> module", at a slight cost.

Right. You want to localise the impact. Using 'open'
is only "poor man's genericity" but a localised version
would be better than nothing.

Interestingly Felix supports that, and it is precisely
how typeclasses passed to functions are implemented:

	fun f[t with Eq[t]] (a:t, b:t, c:t) =>
		a < b and b < c
	;

	// same as "f: Eq t => t :: t * t -> t" in Haskell?

is actually implemented by

		open Eq[t];
		return a < b and b < c;

So in Ocaml if you could also "pass" in the module to be
opened it would be really cool! This should not require
properly first class modules: Felix does it without
them so Ocaml could too :)

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

Re: [Caml-list] Polymorphic Variants

[Tom]

[-- Attachment #1: Type: text/plain, Size: 2342 bytes --]

> Both reasons have practical impact. For the first one, using erasure
> semantics means that the programmer also can discard types when
> understanding the runtime behaviour of a program.


Actually, what I had in mind is exclusivelly compile-time overloading, which
causes no overheed at runtime.




> > Hm... Actually, what I had in mind is nominal subtyping... similar to
> > objects, in fact, objects in C++-like languages, just that they have no
> > class methods.
>
> Reading the description below, this all looks nice, independently of
> the semantics limitation described above. However, you can kiss
> farewell to type inference. With such an extensive overloading, you
> would need type annotations all over the place.
>

For the second one,
> you can write code that is maximally polymorphic, without too much
> fear about the impact of performance (equality is overloaded, so
> it still matters...) or strange ambiguity-related error messages.



I believe that "strange ambiguity-related error messages" are the result of
stupid programmers, not of the language. If one is careful to design a sane
library, most ambiguities never happen! Besides, incorporating whole-program
analysis (in the spirit of MLton), one can postpone such errors until the
whole application has been written, so for example local ambiguities would
be resolved by examining the uses (if a function is always called with
arguments of single type, there is no ambiguity).


> Not for records, but for objects. From a type-theoretic point of view
> they are just equivalent.





> By the way, this all looks likes the "used this feature in C++"
> syndrome. Sure C++ is incredibly powerful. But it is built on rather
> shaky theoretical fundations. So you can't expect to bring everything
> from C++ to a new language. Why not think about new ways to solve
> problems :-)


Well, I am... but just as you are in your message mentioning the practical
impact, so am I. And I think that every way to implement subtyping of
records/objects (=named tuples) other than the C++ way has an important
practical consequence - it's just slow. I guess that C++ like index-based
access is much faster than name-based access neccessary for structural
subtyping. Thou, please prove me that I am wrong :) I want structural
subtyping, the OCaml way, just very fast.

- Tom

[-- Attachment #2: Type: text/html, Size: 3310 bytes --]