* ambitious proposal: polymorphic arithmetics
@ 2005-04-06 15:15 Eijiro Sumii
2005-04-06 15:51 ` [Caml-list] " Sébastien Hinderer
` (5 more replies)
0 siblings, 6 replies; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-06 15:15 UTC (permalink / raw)
To: caml-list; +Cc: sumii
Hi once again,
Well, I asked the same question many years ago, but I'm afraid I
didn't receive satisfactory answers at that time, perhaps because I
was just a nameless student.:-) Now that my colleagues and I won the
ICFP programming contest twice (as well as organizing it once) and
published two POPL papers, I dare to raise the same question again,
hoping I'll receive more reasonable responses this time...;-)
So here it goes: why don't we have polymorphic +, -, etc. while we
have polymorphic =, <, etc.? Many novices and (at least) some experts
feel that +., -., etc. are not quite nice. Why not define +, -,
etc. for as many types as possible such as integers, floating-point
numbers, and tuples? I think they can be implemented almost in the
same efficient way as =. They can also raise an exception if applied
to unsupported values such as functions, just as = does.
P.S. I believe I'm not proposing anything as serious as Haskell type
classes.
--
Eijiro Sumii (http://www.cis.upenn.edu/~sumii/)
Department of Computer and Information Science, University of Pennsylvania
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 15:15 ambitious proposal: polymorphic arithmetics Eijiro Sumii
@ 2005-04-06 15:51 ` Sébastien Hinderer
2005-04-06 15:56 ` Richard Jones
` (4 subsequent siblings)
5 siblings, 0 replies; 25+ messages in thread
From: Sébastien Hinderer @ 2005-04-06 15:51 UTC (permalink / raw)
To: caml-list, caml-list
Hi,
> So here it goes: why don't we have polymorphic +, -, etc. while we
> have polymorphic =, <, etc.? Many novices and (at least) some experts
> feel that +., -., etc. are not quite nice. Why not define +, -,
> etc. for as many types as possible such as integers, floating-point
> numbers, and tuples? I think they can be implemented almost in the
> same efficient way as =. They can also raise an exception if applied
> to unsupported values such as functions, just as = does.
By the way, why isn't it possible to detect this kind of errors at
compile-time ?
Isn't the type-system strong enough ?
> P.S. I believe I'm not proposing anything as serious as Haskell type
> classes.
I was wondering if it would be theoretically possible to have
Haskell-like type classes in Caml ?
If it is possible in theory, is it something Caml developers plan to
implement, one day ?
Thanks,
Sébastien.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 15:15 ambitious proposal: polymorphic arithmetics Eijiro Sumii
2005-04-06 15:51 ` [Caml-list] " Sébastien Hinderer
@ 2005-04-06 15:56 ` Richard Jones
2005-04-06 16:43 ` Dmitry Lomov
2005-04-06 16:39 ` [Caml-list] " William Lovas
` (3 subsequent siblings)
5 siblings, 1 reply; 25+ messages in thread
From: Richard Jones @ 2005-04-06 15:56 UTC (permalink / raw)
To: Eijiro Sumii; +Cc: caml-list, sumii
The problem, I'm guessing, is that you add polymorphic +, -, and so
on. But that's really just a hack in the language. Sooner or later
people are going to ask why it's not possible to write a polymorphic
'print' function, _without_ hacking the language some more. At that
point you need a theory, and you need something like G'Caml, or type
classes, or GADTS.
Rich.
--
Richard Jones, CTO Merjis Ltd.
Merjis - web marketing and technology - http://merjis.com
Team Notepad - intranets and extranets for business - http://team-notepad.com
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 15:15 ambitious proposal: polymorphic arithmetics Eijiro Sumii
2005-04-06 15:51 ` [Caml-list] " Sébastien Hinderer
2005-04-06 15:56 ` Richard Jones
@ 2005-04-06 16:39 ` William Lovas
2005-04-06 16:59 ` Andreas Rossberg
` (2 more replies)
2005-04-06 17:00 ` Christophe TROESTLER
` (2 subsequent siblings)
5 siblings, 3 replies; 25+ messages in thread
From: William Lovas @ 2005-04-06 16:39 UTC (permalink / raw)
To: caml-list
Hi Eijiro,
On Wed, Apr 06, 2005 at 11:15:05AM -0400, Eijiro Sumii wrote:
> So here it goes: why don't we have polymorphic +, -, etc. while we
> have polymorphic =, <, etc.? Many novices and (at least) some experts
> feel that +., -., etc. are not quite nice. Why not define +, -,
> etc. for as many types as possible such as integers, floating-point
> numbers, and tuples? I think they can be implemented almost in the
> same efficient way as =. They can also raise an exception if applied
> to unsupported values such as functions, just as = does.
Many experts (and perhaps some novices *shrug*) think that polymorphic
equality is a bad idea... so maybe it's best to just leave "well enough"
alone :)
More seriously, one might argue -- only slightly hand-wavily -- that with
=, <, etc., types whose values *cannot* be used as inputs are the exception
rather than the rule, whereas the reverse is the case for +, -, etc. For
example, it may be perfectly clear (or at least possible to specify) how to
implement comparisons on data types, records, and tuples. What should the
arithmetic operators mean on such things? (This argument breaks down in
the face of code which relies on abstract types to enforce modularity -- in
such cases, incomparability can become "the rule" rather than the
exception, putting =, <, etc. on the same footing as +, -, etc.)
These are just my thoughts, though, and i'm still something of a nameless
student :)
cheers,
William
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 15:56 ` Richard Jones
@ 2005-04-06 16:43 ` Dmitry Lomov
2005-04-06 18:59 ` Richard Jones
0 siblings, 1 reply; 25+ messages in thread
From: Dmitry Lomov @ 2005-04-06 16:43 UTC (permalink / raw)
To: caml-list
Richard Jones wrote:
> The problem, I'm guessing, is that you add polymorphic +, -, and so
> on. But that's really just a hack in the language. Sooner or later
> people are going to ask why it's not possible to write a polymorphic
> 'print' function, _without_ hacking the language some more. At that
> point you need a theory, and you need something like G'Caml, or type
> classes, or GADTS.
Pardon my ignorance, but how are GADTs are going to help in this regard?
I thought GADTs are basically data types with constructors that have
non-uniform "return type".
Friendly,
Dmitry
--
Dmitry Lomov
JetBrains Inc.
http://www.jetbrains.com
"Develop With Pleasure!"
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 16:39 ` [Caml-list] " William Lovas
@ 2005-04-06 16:59 ` Andreas Rossberg
2005-04-06 18:50 ` Eijiro Sumii
2005-04-06 19:33 ` Eijiro Sumii
2 siblings, 0 replies; 25+ messages in thread
From: Andreas Rossberg @ 2005-04-06 16:59 UTC (permalink / raw)
To: caml-list
William Lovas wrote:
>
> (This argument breaks down in
> the face of code which relies on abstract types to enforce modularity -- in
> such cases, incomparability can become "the rule" rather than the
> exception, putting =, <, etc. on the same footing as +, -, etc.)
In fact, the polymorphic approach would make abstract types comparable
if their representation is, hence the idea of (non-parametric)
polymorphic operations of this sort slaps right in the face of type
abstraction and encapsulation, which are high values of ML.
Cheers,
- Andreas
--
Andreas Rossberg, rossberg@ps.uni-sb.de
Let's get rid of those possible thingies! -- TB
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 15:15 ambitious proposal: polymorphic arithmetics Eijiro Sumii
` (2 preceding siblings ...)
2005-04-06 16:39 ` [Caml-list] " William Lovas
@ 2005-04-06 17:00 ` Christophe TROESTLER
2005-04-06 19:20 ` Eijiro Sumii
2005-04-06 17:23 ` Marcin 'Qrczak' Kowalczyk
2005-04-09 2:58 ` Jon Harrop
5 siblings, 1 reply; 25+ messages in thread
From: Christophe TROESTLER @ 2005-04-06 17:00 UTC (permalink / raw)
To: eijiro_sumii; +Cc: caml-list, sumii
On Wed, 06 Apr 2005, Eijiro Sumii <eijiro_sumii@anet.ne.jp> wrote:
>
Well, I am not anywhere as much known as you are in the FP community
but let me jump in anyway! :)
> So here it goes: why don't we have polymorphic +, -, etc. while we
> have polymorphic =, <, etc.? [...] define +, -, etc. for as many
> types as possible such as integers, floating-point numbers, and tuples?
IMHO, the problem is not that much to have an handy set of polymorphic
operators than to be able to _extend_ them. See for example
http://cvs.alioth.debian.org/cgi-bin/cvsweb.cgi/shootout/bench/implicitode/implicitode.ocaml?rev=1.2&content-type=text/x-cvsweb-markup&cvsroot=shootout
for a use of [open] and [let ... and ...] at the right places for the
expressions to look "nice" (e.g. [a * b] instead of [M.( * ) a b]).
In the mathematical world, this need occurs all the time. E.g. you
define finite fields and want +, =,... to operate on those. You also
want to define generic algorithms with those notions, e.g. power (as
of now, functors would be used for this). The main difficulties
currently are that (1) it is difficult to use [open] at the right
places -- I have not checked whether the "openin" camlp4 extension can
handle unary and binary operators -- and (2) mixing the operators in a
single expression is impossible -- e.g. (a * b) * matrix. However, I
would strongly like all this to be statically type checked -- no
exceptions _please_. In fact, provided a suitable mechanism is found,
I would like = to stop throwing exceptions.
Personally I do not mid about +., *.,... even though admittedly they
are odd at the beginning. But if 1 + 1.2 is going to throw an
exception, this is far far worse (simple typing mistakes will now
"crash" the program!!!).
> P.S. I believe I'm not proposing anything as serious as Haskell type
> classes.
Imagine how
val plus : [| int -> int -> int
| float -> float -> float |] = <generic>
will look once there are 10 types. This is going to be even worse if
equality is to be _completely_ statically checked (as I desire). I
only know superficially type classes, but
(=) : Eq 'a => 'a -> 'a -> bool
is much more readable than
(=) : [| int -> int -> bool
| float -> float -> bool
| 'a list -> 'a list -> bool
| ... |]
Moreover and more importantly, they can be extended (e.g. add Num.num
to the Eq class). Also, "subclassing" should be possible (e.g. Ordered 'a
=> Eq 'a). We are not allowing capitalized type names; this is a good
opportunity to use them!
In summary (since the opened the Pandora box), it would be nice if a
solution would be found to this "problem" but, let's go for a general
and useful one, not an had-oc one. :)
Regards,
ChriS
---
P.S. Maybe GADTs provide an alternative solution for named functions
but I believe not for binary operators.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 15:15 ambitious proposal: polymorphic arithmetics Eijiro Sumii
` (3 preceding siblings ...)
2005-04-06 17:00 ` Christophe TROESTLER
@ 2005-04-06 17:23 ` Marcin 'Qrczak' Kowalczyk
2005-04-06 18:01 ` padiolea
2005-04-09 2:58 ` Jon Harrop
5 siblings, 1 reply; 25+ messages in thread
From: Marcin 'Qrczak' Kowalczyk @ 2005-04-06 17:23 UTC (permalink / raw)
To: caml-list
Eijiro Sumii <eijiro_sumii@anet.ne.jp> writes:
> So here it goes: why don't we have polymorphic +, -, etc. while we
> have polymorphic =, <, etc.?
=, < have type 'a -> 'a -> bool, so they appear to be applicable
to *all* types. It happens that their implementation doesn't need
to distinguish different types which currently have the same
representation, it just examines the representation at runtime. 0 < 1
uses the same code as false < true.
(Modulo special code generated based on the static type when it's
known, but in polymorphic functions it is not known, so this must be
optional, can't be relied on.)
+ can't be treated in the same way, because it won't distinguish
whether it's called as 1 + 1 or true + true. If it returns 2 in the
former case, it would produce a nonsensical bool value in the latter
case.
OCaml doesn't have a mechanism for making +, - applicable to a limited
set of types and for dispatching their implementation based on the type
rather than on the physical representation.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 17:23 ` Marcin 'Qrczak' Kowalczyk
@ 2005-04-06 18:01 ` padiolea
2005-04-06 19:14 ` Eijiro Sumii
2005-04-06 19:23 ` Richard Jones
0 siblings, 2 replies; 25+ messages in thread
From: padiolea @ 2005-04-06 18:01 UTC (permalink / raw)
To: Marcin 'Qrczak' Kowalczyk; +Cc: caml-list
> Eijiro Sumii <eijiro_sumii@anet.ne.jp> writes:
>
>> So here it goes: why don't we have polymorphic +, -, etc. while we
>> have polymorphic =, <, etc.?
>
[...]
>
> OCaml doesn't have a mechanism for making +, - applicable to a limited
> set of types and for dispatching their implementation based on the type
> rather than on the physical representation.
In the module Obj of the caml library there is a function
external is_int : t -> bool = "%obj_is_int"
I guess that the value are represented internally as "cells" and that
cells have a bit indicating wether it is an int or a pointer (and also
a bit for the gc)
By using more bits we could know wether or not it is a float, and
so have also a function
is_float: t -> bool
and so we could then code a "generic" + function
(but it would lead to an overhead due to the dispatch).
Nevertheless I dont think that making + generic is an ambitious/important
feature.
My big wish for ocaml would be to have some better tracing facilities,
a generic print function, and the possibilty to print backtraces,
some features available in langage such as perl and that makes the life
of the developper far easier.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 16:39 ` [Caml-list] " William Lovas
2005-04-06 16:59 ` Andreas Rossberg
@ 2005-04-06 18:50 ` Eijiro Sumii
2005-04-06 19:33 ` Eijiro Sumii
2 siblings, 0 replies; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-06 18:50 UTC (permalink / raw)
To: caml-list; +Cc: sumii
Thanks to everybody for the excitements!:-)
From: "William Lovas" <wlovas@stwing.upenn.edu>
> Many experts (and perhaps some novices *shrug*) think that polymorphic
> equality is a bad idea...
I'm almost tempted to agree.:-) As other responses have also
suggested, the issue seems to be "where to draw the line." If so, I
can perhaps restate my question as: why is the line drawn between =
and + now? Is it the best?
Eijiro
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 16:43 ` Dmitry Lomov
@ 2005-04-06 18:59 ` Richard Jones
2005-04-06 19:19 ` Jacques Carette
2005-04-07 0:01 ` Ethan Aubin
0 siblings, 2 replies; 25+ messages in thread
From: Richard Jones @ 2005-04-06 18:59 UTC (permalink / raw)
Cc: caml-list
On Wed, Apr 06, 2005 at 08:43:01PM +0400, Dmitry Lomov wrote:
> Richard Jones wrote:
> >The problem, I'm guessing, is that you add polymorphic +, -, and so
> >on. But that's really just a hack in the language. Sooner or later
> >people are going to ask why it's not possible to write a polymorphic
> >'print' function, _without_ hacking the language some more. At that
> >point you need a theory, and you need something like G'Caml, or type
> >classes, or GADTS.
>
> Pardon my ignorance, but how are GADTs are going to help in this regard?
> I thought GADTs are basically data types with constructors that have
> non-uniform "return type".
Pardon _my_ ignorance. I read something about using GADTs to simulate
class types in the paper, and assumed that they are equivalent, but
I'm probably wrong.
Rich.
--
Richard Jones, CTO Merjis Ltd.
Merjis - web marketing and technology - http://merjis.com
Team Notepad - intranets and extranets for business - http://team-notepad.com
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 18:01 ` padiolea
@ 2005-04-06 19:14 ` Eijiro Sumii
2005-04-06 20:31 ` Eijiro Sumii
2005-04-06 19:23 ` Richard Jones
1 sibling, 1 reply; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-06 19:14 UTC (permalink / raw)
To: caml-list; +Cc: sumii
From: "Marcin 'Qrczak' Kowalczyk" <qrczak@knm.org.pl>
| + can't be treated in the same way, because it won't distinguish
| whether it's called as 1 + 1 or true + true. If it returns 2 in the
| former case, it would produce a nonsensical bool value in the latter
| case.
|
| OCaml doesn't have a mechanism for making +, - applicable to a limited
| set of types and for dispatching their implementation based on the type
| rather than on the physical representation.
This is an excellent point. (Somebody else also pointed it out in a
reply to me.)
From: padiolea@irisa.fr
> In the module Obj of the caml library there is a function
> external is_int : t -> bool = "%obj_is_int"
But it doesn't quite work for our purpose here, for example:
# type t = A | B ;;
type t = A | B
# Obj.is_int (Obj.magic A) ;;
- : bool = true
Eijiro
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 18:59 ` Richard Jones
@ 2005-04-06 19:19 ` Jacques Carette
2005-04-07 0:01 ` Ethan Aubin
1 sibling, 0 replies; 25+ messages in thread
From: Jacques Carette @ 2005-04-06 19:19 UTC (permalink / raw)
To: Richard Jones; +Cc: caml-list
Richard Jones <rich@annexia.org> wrote:
> > Pardon my ignorance, but how are GADTs are going to help in this regard?
> > I thought GADTs are basically data types with constructors that have
> > non-uniform "return type".
>
> Pardon _my_ ignorance. I read something about using GADTs to simulate
> class types in the paper, and assumed that they are equivalent, but
> I'm probably wrong.
GADTs have non-uniform input *and* output types. But the non-uniformity still has enough regularity to it that this
does not give full sub-typing or dependent types (both of which are much harder). They are a really beautiful
extension of algebraic types in the 'dependent types' direction without introducing anything harder than what is
already present in the type system. The chapter by Pottier and Re'my in ATTAPL pretty much admits that in writing ;-)
So maybe the Ocaml developers have been working hard on this for ocaml 3.09, they just didn't want to tip their hats
quite yet...
Certainly GADTs are sufficient for statically typing an embedded language *and* [the important part] its 'cannot go
wrong' interpreter that follows purely from the operational semantics. The leap from that to controlled, non ad hoc
polymorphic + seems quite small.
So if the types on which you are working are tagged, then GADTs could well help. Of course, for performance and
historical reasons, int are not tagged in Ocaml, so that is a definite problem. But perhaps the 'untagging' of
integers is done late enough in the compilation process (I don't know!) that it is not a real problem.
Jacques
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 17:00 ` Christophe TROESTLER
@ 2005-04-06 19:20 ` Eijiro Sumii
2005-04-07 14:00 ` Christophe TROESTLER
0 siblings, 1 reply; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-06 19:20 UTC (permalink / raw)
To: caml-list; +Cc: sumii
From: Christophe TROESTLER <debian00@tiscali.be>
> But if 1 + 1.2 is going to throw an exception, this is far far worse
> (simple typing mistakes will now "crash" the program!!!).
It doesn't, just as "1 = 1.2" doesn't - they are both compile-time
errors.
> In summary (since the opened the Pandora box), it would be nice if a
> solution would be found to this "problem" but, let's go for a general
> and useful one, not an had-oc one. :)
I agree my proposal is ad hoc - and a better solution would be better,
if possible!:-)
Eijiro
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 18:01 ` padiolea
2005-04-06 19:14 ` Eijiro Sumii
@ 2005-04-06 19:23 ` Richard Jones
1 sibling, 0 replies; 25+ messages in thread
From: Richard Jones @ 2005-04-06 19:23 UTC (permalink / raw)
To: caml-list
On Wed, Apr 06, 2005 at 08:01:00PM +0200, padiolea@irisa.fr wrote:
> In the module Obj of the caml library there is a function
> external is_int : t -> bool = "%obj_is_int"
> I guess that the value are represented internally as "cells" and that
> cells have a bit indicating wether it is an int or a pointer (and also
> a bit for the gc)
Internally as "values". The LSB indicates whether a value is an int
or a pointer to something boxed. (LSB = 1 => int). For boxed data
the header tells you what it is and how big it is.
> By using more bits we could know wether or not it is a float, and
> so have also a function
> is_float: t -> bool
> and so we could then code a "generic" + function
Floats are normally stored boxed, except when they happen to be in
registers, or they are stored in an array.
Anyway, it's already possible to write some generic functions,
provided you confine yourself to the type information available at
runtime. For example, a slow generic (+) is:
open Printf
type t = Int of int | Float of float
let (+) a b =
let get_type v =
let r = Obj.repr v in
if Obj.is_int r then
Int (Obj.magic r : int)
else if Obj.size r = 2 && Obj.tag r = Obj.double_tag then
Float (Obj.magic r : float)
else (
prerr_endline ("size = " ^ string_of_int (Obj.size r) ^ ", tag = " ^
string_of_int (Obj.tag r));
invalid_arg "(+): arguments must have type int or float"
)
in
match get_type a, get_type b with
| Int a, Int b -> Int (a + b)
| Float a, Float b -> Float (a +. b)
| Int a, Float b -> Float (float a +. b)
| Float a, Int b -> Float (a +. float b)
let string_of_t = function
| Int a -> string_of_int a
| Float a -> string_of_float a
let () =
print_endline (string_of_t (1 + 2));
print_endline (string_of_t (1. + 2));
print_endline (string_of_t (1 + 2.));
print_endline (string_of_t (1. + 2.))
See also the function 'dump' in:
http://cvs.sourceforge.net/viewcvs.py/ocaml-lib/extlib-dev/std.ml?rev=1.15&view=markup
> My big wish for ocaml would be to have some better tracing facilities,
> a generic print function, and the possibilty to print backtraces,
Being able to print full backtraces (with function names and
parameters) would be just great.
Rich.
--
Richard Jones, CTO Merjis Ltd.
Merjis - web marketing and technology - http://merjis.com
Team Notepad - intranets and extranets for business - http://team-notepad.com
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 16:39 ` [Caml-list] " William Lovas
2005-04-06 16:59 ` Andreas Rossberg
2005-04-06 18:50 ` Eijiro Sumii
@ 2005-04-06 19:33 ` Eijiro Sumii
2005-04-07 0:13 ` William Lovas
2 siblings, 1 reply; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-06 19:33 UTC (permalink / raw)
To: caml-list; +Cc: sumii
From: "William Lovas" <wlovas@stwing.upenn.edu>
> More seriously, one might argue -- only slightly hand-wavily -- that with
> =, <, etc., types whose values *cannot* be used as inputs are the exception
> rather than the rule, whereas the reverse is the case for +, -, etc. For
> example, it may be perfectly clear (or at least possible to specify) how to
> implement comparisons on data types, records, and tuples. What should the
> arithmetic operators mean on such things?
I don't quite think comparisons are clearer (or "more possible" to
specify) than additions for tuples and records - they can be defined
just element-wise. Data types indeed seem more problematic as pointed
out in other replies.
> (This argument breaks down in
> the face of code which relies on abstract types to enforce modularity -- in
> such cases, incomparability can become "the rule" rather than the
> exception, putting =, <, etc. on the same footing as +, -, etc.)
Yes, polymorphic comparison already breaks type abstraction.
Eijiro
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 19:14 ` Eijiro Sumii
@ 2005-04-06 20:31 ` Eijiro Sumii
2005-04-06 21:53 ` Marcin 'Qrczak' Kowalczyk
0 siblings, 1 reply; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-06 20:31 UTC (permalink / raw)
To: caml-list; +Cc: sumii
P.S.
> From: "Marcin 'Qrczak' Kowalczyk" <qrczak@knm.org.pl>
> | + can't be treated in the same way, because it won't distinguish
> | whether it's called as 1 + 1 or true + true. If it returns 2 in the
> | former case, it would produce a nonsensical bool value in the latter
> | case.
> |
> | OCaml doesn't have a mechanism for making +, - applicable to a limited
> | set of types and for dispatching their implementation based on the type
> | rather than on the physical representation.
>
> This is an excellent point. (Somebody else also pointed it out in a
> reply to me.)
Since this seems to be the most serious issue, I checked what could
happen in slightly greater detail.
----------------------------------------------------------------------
Objective Caml version 3.08.2
# let c = (Obj.magic (Obj.magic true + Obj.magic true) : bool) ;;
val c : bool = <unknown constructor>
# if c then 123 else 456 ;;
- : int = 123
# type t = A | B ;;
type t = A | B
# let d = (Obj.magic (Obj.magic B + Obj.magic B) : t) ;;
val d : t = <unknown constructor>
# (function A -> 78 | B -> 90) d ;;
- : int = 90
#
----------------------------------------------------------------------
So, it indeed leads to "unknown" values and behaviors, but doesn't
seem to break memory safety (in this case, at least). This may or may
not be regarded as something similar to the "undefined" (or only
partially specified) behavior of Pervasives.compare for function
values.
Or are there actually other cases where even memory safety can be
broken?
Eijiro
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 20:31 ` Eijiro Sumii
@ 2005-04-06 21:53 ` Marcin 'Qrczak' Kowalczyk
2005-04-06 22:38 ` Eijiro Sumii
0 siblings, 1 reply; 25+ messages in thread
From: Marcin 'Qrczak' Kowalczyk @ 2005-04-06 21:53 UTC (permalink / raw)
To: caml-list
Eijiro Sumii <eijiro_sumii@anet.ne.jp> writes:
> # let d = (Obj.magic (Obj.magic B + Obj.magic B) : t) ;;
> val d : t = <unknown constructor>
> # (function A -> 78 | B -> 90) d ;;
> - : int = 90
> #
> ----------------------------------------------------------------------
>
> So, it indeed leads to "unknown" values and behaviors, but doesn't
> seem to break memory safety (in this case, at least).
# type t = A | B | C;;
type t = A | B | C
# match (Obj.magic (Obj.magic C + Obj.magic C)) with A -> 0 | B -> 1 | C -> 2;;
zsh: segmentation fault ocaml
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 21:53 ` Marcin 'Qrczak' Kowalczyk
@ 2005-04-06 22:38 ` Eijiro Sumii
0 siblings, 0 replies; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-06 22:38 UTC (permalink / raw)
To: caml-list; +Cc: sumii
From: "Marcin 'Qrczak' Kowalczyk" <qrczak@knm.org.pl>
> # type t = A | B | C;;
> type t = A | B | C
> # match (Obj.magic (Obj.magic C + Obj.magic C)) with A -> 0 | B -> 1 | C -> 2;;
> zsh: segmentation fault ocaml
Good job!! It reproduced in all environments I have access to. Then,
after all, "polymorphic addition" isn't actually as easy to implement
in OCaml as I (rather naively) thought...
Thanks so much to everybody for the very informative responses!
Eijiro
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: ambitious proposal: polymorphic arithmetics
2005-04-06 18:59 ` Richard Jones
2005-04-06 19:19 ` Jacques Carette
@ 2005-04-07 0:01 ` Ethan Aubin
1 sibling, 0 replies; 25+ messages in thread
From: Ethan Aubin @ 2005-04-07 0:01 UTC (permalink / raw)
To: caml-list
Gadts can do for all sorts of cool things. For example, an approach to
simulate type classes with gadts see
http://www.cs.bu.edu/~hwxi/GRecTypecon/PAPER/main.pdf, to create a
statically typed printf see
http://www.cs.bu.edu/~hwxi/academic/papers/popl03.pdf
Hongwei Xi and Tim Sheard's papers have tons of interesting examples
in their publications. I hope some ideas from their languages, ATS and
Omega respectively, trickle down to Ocaml.
> On Wed, Apr 06, 2005 at 08:43:01PM +0400, Dmitry Lomov wrote:
>> Richard Jones wrote:
>> >The problem, I'm guessing, is that you add polymorphic +, -, and so
>> >on. But that's really just a hack in the language. Sooner or later
>> >people are going to ask why it's not possible to write a polymorphic
>> >'print' function, _without_ hacking the language some more. At that
>> >point you need a theory, and you need something like G'Caml, or type
>> >classes, or GADTS.
>>
>> Pardon my ignorance, but how are GADTs are going to help in this regard?
>> I thought GADTs are basically data types with constructors that have
>> non-uniform "return type".
> Pardon _my_ ignorance. I read something about using GADTs to simulate
> class types in the paper, and assumed that they are equivalent, but
> I'm probably wrong.
Also, sorry for any duplicate post.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 19:33 ` Eijiro Sumii
@ 2005-04-07 0:13 ` William Lovas
2005-04-07 1:58 ` Jacques Garrigue
0 siblings, 1 reply; 25+ messages in thread
From: William Lovas @ 2005-04-07 0:13 UTC (permalink / raw)
To: caml-list
On Wed, Apr 06, 2005 at 03:33:56PM -0400, Eijiro Sumii wrote:
> From: "William Lovas" <wlovas@stwing.upenn.edu>
> > (This argument breaks down in
> > the face of code which relies on abstract types to enforce modularity -- in
> > such cases, incomparability can become "the rule" rather than the
> > exception, putting =, <, etc. on the same footing as +, -, etc.)
>
> Yes, polymorphic comparison already breaks type abstraction.
I did not realize this! Can somebody explain the following interactions?
# let r = Ratio.ratio_of_int 5;;
val r : Ratio.ratio = <abstr>
# r = r;;
Exception: Invalid_argument "equal: abstract value".
# module M : sig type t;; val of_int : int -> t end =
struct type t = int;; let of_int x = x end;;
module M : sig type t val of_int : int -> t end
# let t = M.of_int 5;;
val t : M.t = <abstr>
# t = t;;
- : bool = true
I thought that perhaps all comparisons of abstract values resulted in a
runtime error, but evidently i was mistaken :/ What's the secret to making
a type "really" abstract?
William
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-07 0:13 ` William Lovas
@ 2005-04-07 1:58 ` Jacques Garrigue
0 siblings, 0 replies; 25+ messages in thread
From: Jacques Garrigue @ 2005-04-07 1:58 UTC (permalink / raw)
To: wlovas; +Cc: caml-list
From: William Lovas <wlovas@stwing.upenn.edu>
> > Yes, polymorphic comparison already breaks type abstraction.
>
> I did not realize this! Can somebody explain the following interactions?
>
> # let r = Ratio.ratio_of_int 5;;
> val r : Ratio.ratio = <abstr>
> # r = r;;
> Exception: Invalid_argument "equal: abstract value".
>
> # module M : sig type t;; val of_int : int -> t end =
> struct type t = int;; let of_int x = x end;;
> module M : sig type t val of_int : int -> t end
> # let t = M.of_int 5;;
> val t : M.t = <abstr>
> # t = t;;
> - : bool = true
>
> I thought that perhaps all comparisons of abstract values resulted in a
> runtime error, but evidently i was mistaken :/ What's the secret to making
> a type "really" abstract?
The error message is a bit misleading: it actually means an internal
object with abstract tag. You can only produce those on the C side.
However, this gives you a trick if you want to protect a type from
comparisons: include an incomparable field in it. Better to put it as
first field, as it then makes sure that even ordering cannot be be
checked.
type 'a protected = {prot: unit Weak.t; desc: 'a}
let protect d = {prot = Weak.create 1; desc = d }
Now protected values are impossible to compare.
More precisely, they are only comparable when physically equal, which
you can anyway check with ==. Even in this case polymorphic equality
will fail (it checks even physically equal values.)
# let x = protect 1;;
val x : int protected = {prot = <abstr>; desc = 1}
# x=x;;
Exception: Invalid_argument "equal: abstract value".
# compare x x;;
- : int = 0
# let y = protect 1;;
val y : int protected = {prot = <abstr>; desc = 1}
# compare x y;;
Exception: Invalid_argument "equal: abstract value".
So, if you really need abstraction, you can have it.
(You can still break it using the Obj module, but this is another
story...)
Jacques Garrigue
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 19:20 ` Eijiro Sumii
@ 2005-04-07 14:00 ` Christophe TROESTLER
0 siblings, 0 replies; 25+ messages in thread
From: Christophe TROESTLER @ 2005-04-07 14:00 UTC (permalink / raw)
To: caml-list; +Cc: eijiro_sumii, sumii
On Wed, 06 Apr 2005, Eijiro Sumii <eijiro_sumii@anet.ne.jp> wrote:
>
> > But if 1 + 1.2 is going to throw an exception
> It doesn't, just as "1 = 1.2" doesn't - they are both compile-time errors.
My mistake. Thanks for the correction.
> From: "William Lovas" <wlovas@stwing.upenn.edu>
> > Many experts (and perhaps some novices *shrug*) think that polymorphic
> > equality is a bad idea...
>
> I'm almost tempted to agree.:-) As other responses have also
> suggested, the issue seems to be "where to draw the line." If so, I
> can perhaps restate my question as: why is the line drawn between =
> and + now? Is it the best?
I'd like to ask from a non-expert standpoint: what would be the
advantages and drawbacks of something like type classes for OCaml?
Also, how do they compare with GCaml (in terms of flexibility,
extensibility, efficiency,...)?
Regards,
ChriS
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-06 15:15 ambitious proposal: polymorphic arithmetics Eijiro Sumii
` (4 preceding siblings ...)
2005-04-06 17:23 ` Marcin 'Qrczak' Kowalczyk
@ 2005-04-09 2:58 ` Jon Harrop
2005-04-09 3:16 ` Eijiro Sumii
5 siblings, 1 reply; 25+ messages in thread
From: Jon Harrop @ 2005-04-09 2:58 UTC (permalink / raw)
To: caml-list
On Wednesday 06 April 2005 16:15, Eijiro Sumii wrote:
> So here it goes: why don't we have polymorphic +, -, etc. while we
> have polymorphic =, <, etc.? Many novices and (at least) some experts
> feel that +., -., etc. are not quite nice. Why not define +, -,
> etc. for as many types as possible such as integers, floating-point
> numbers, and tuples? I think they can be implemented almost in the
> same efficient way as =. They can also raise an exception if applied
> to unsupported values such as functions, just as = does.
I'm just curious, but what would you have expected the result of:
# (1, 2, 3) * (2, 3, 4);;
to be? i.e. an inner product, element-wise multiplication or an outer product?
> P.S. I believe I'm not proposing anything as serious as Haskell type
> classes.
Oh, this isn't serious? ;-)
> If so, I can perhaps restate my question as: why is the line drawn between =
> and + now?
I would say that polymorphic comparisons are useful in many more circumstances
than polymorphic arithmetics would be, so their inclusion is justified.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [Caml-list] ambitious proposal: polymorphic arithmetics
2005-04-09 2:58 ` Jon Harrop
@ 2005-04-09 3:16 ` Eijiro Sumii
0 siblings, 0 replies; 25+ messages in thread
From: Eijiro Sumii @ 2005-04-09 3:16 UTC (permalink / raw)
To: caml-list; +Cc: Jon Harrop
> I'm just curious, but what would you have expected the result of:
>
> # (1, 2, 3) * (2, 3, 4);;
>
> to be? i.e. an inner product, element-wise multiplication or an outer product?
Right, it is one of the difficult cases, but in general I just had
simple element-wise operations (of type 'a -> 'a -> 'a) in mind.
> > If so, I can perhaps restate my question as: why is the line drawn between =
> > and + now?
>
> I would say that polymorphic comparisons are useful in many more circumstances
> than polymorphic arithmetics would be, so their inclusion is justified.
Yes, I agree polymorphic equality can be more useful in practice,
though I'm not very sure about polymorphic inequalities (perhaps
except for the purpose of ordering when implementing containers such
as sets, trees, ...), in particular concerning abstract types as
somebody else mentioned...?
Eijiro
^ permalink raw reply [flat|nested] 25+ messages in thread
end of thread, other threads:[~2005-04-09 3:16 UTC | newest]
Thread overview: 25+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2005-04-06 15:15 ambitious proposal: polymorphic arithmetics Eijiro Sumii
2005-04-06 15:51 ` [Caml-list] " Sébastien Hinderer
2005-04-06 15:56 ` Richard Jones
2005-04-06 16:43 ` Dmitry Lomov
2005-04-06 18:59 ` Richard Jones
2005-04-06 19:19 ` Jacques Carette
2005-04-07 0:01 ` Ethan Aubin
2005-04-06 16:39 ` [Caml-list] " William Lovas
2005-04-06 16:59 ` Andreas Rossberg
2005-04-06 18:50 ` Eijiro Sumii
2005-04-06 19:33 ` Eijiro Sumii
2005-04-07 0:13 ` William Lovas
2005-04-07 1:58 ` Jacques Garrigue
2005-04-06 17:00 ` Christophe TROESTLER
2005-04-06 19:20 ` Eijiro Sumii
2005-04-07 14:00 ` Christophe TROESTLER
2005-04-06 17:23 ` Marcin 'Qrczak' Kowalczyk
2005-04-06 18:01 ` padiolea
2005-04-06 19:14 ` Eijiro Sumii
2005-04-06 20:31 ` Eijiro Sumii
2005-04-06 21:53 ` Marcin 'Qrczak' Kowalczyk
2005-04-06 22:38 ` Eijiro Sumii
2005-04-06 19:23 ` Richard Jones
2005-04-09 2:58 ` Jon Harrop
2005-04-09 3:16 ` Eijiro Sumii
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox