-
Notifications
You must be signed in to change notification settings - Fork 0
/
2002.12.03.txt
164 lines (129 loc) · 6.86 KB
/
2002.12.03.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
Hello,
Here is the latest Caml Weekly News, week 26 November to 03 December, 2002.
1) OCAMAWEB release
2) Understanding why Ocaml doesn't support operator overloading
3) arbitrarily large integers
======================================================================
1) OCAMAWEB release
----------------------------------------------------------------------
Charles Lehalle announced:
We just release OCAMAWEB in GPL licence at sourceforge
http://ocamaweb.sf.net
OCAMAWEB is a software that produce LaTeX documentation on MATLAB files
with some special comments.
It is written in OCAML.
It is a literate programming tool.
MIRIAD Technologies decided to put it available to the ocaml and matlab
community.
I hope you will use it and send us comments.
======================================================================
2) Understanding why Ocaml doesn't support operator overloading
----------------------------------------------------------------------
A long thread has spawned about Ocaml and operator overloading, starting
at: http://caml.inria.fr/archives/200211/msg00329.html
Here are some hilights.
Jørgen Hermanrud Fjeld asked and Xavier Leroy answered:
> Some time ago, when looking at Ocaml for the first time, I got
> baffled by the lack of operator overloading. I am still wondering
> why this is the case. Could someone please point me to more
> information about this?
> I remember reading something about operator overloading and type inference
> being hard to combine.
I don't know how technical you'd like the answer to be, so let me
start with a simple explanation that doesn't get into all technical
details.
The problem is indeed the combination of overloading and type
inference. The catch-22 is this:
- overloading determines the meaning of an operator from the types of
its arguments (e.g. to determine whether + is integer addition or
floating-point addition);
- type inference relies (among other things) on the fact that each
operator has a unique type to determine the types of its arguments
(e.g. if one of the arguments is a function parameter).
If you don't see the circularity, consider
let f x = x + x
If "+" is overloaded on integers and on floats, you get two possible
types for f: int -> int or float -> float. None of these types is
better than the other; if the compiler commits to one of them, say
int->int, later applications of f (e.g. to a float) can be rejected.
In technical terms, we say that the principal types property fails.
This property says that the inferred type is always the "best" in the
sense that it subsumes all other possible types. Its a crucial
property in order to do type inference, both from a theoretical and a
practical (usability) standpoint.
There are many ways to go about the problem with "f" above.
A simple one is to reject the definition as ambiguous, and require the
programmer to disambiguate, e.g. by putting a type declaration on "x".
Another equally simple is to resolve ambiguities using a default
strategy, e.g. favor "int" over "float". Both ways aren't very nice,
since they break the principal types property.
Many type inference systems have been proposed for overloading that
preserve the principal types property. The most famous example (but
not the only one) is Haskell's type classes. If you look at the
literature, you'll see that they all involve significant typing
machinery; some even have significant impact on the design of the
whole language (as in the case of Haskell). I'm not criticizing here,
just pointing out that combining type inference and overloading is not
a trivial extension of ML-style type inference.
Hope this (partially) answers your question.
Christophe Raffalli added:
Another solution is at
http://pauillac.inria.fr/~furuse/generics/
A question: will this be available in future official release of OCaml ?
Pierre Weis said and Christophe Raffalli answered:
> Yes: I suspect a really nasty corner in this area. As far as I
> remember, the kind of types you suggest is known as ``intersection
> types'', and the type reconstruction problem for languages featuring
> those types is just undecidable. The big problem with this kind of
> stuff is to restrict the type schemes allowed in your type system such
> that you do not fall into the undecidable general case, while still
> maintaining a powerful enough type system to properly typecheck the
> function double (fun x -> x + x).
>
This is not the only solution: another solution is to keep the simple (in the
definition) type system with an incomplete algorithm that will always succeed
if enough type information. This works for instance for Mitchell's system F
with subtyping (see my normaliser:
http://lama-d134.univ-savoie.fr/~raffalli/normaliser.html)
The difficulty is that you need to have a very good way of printing
typing error message so that the user can easily guess where to add type
information until it works or a real error in the code is detected.
Recent work (in a simple setting) by Christian Haack, and Joe Wells
http://www.cee.hw.ac.uk/ultra/compositional-analysis/type-error-slicing
let me think that there may be a (non trivial) solution.
The big advantage, is that there are (undecidable) type systems that can
unifies typing of record, modules and object; functor and functions. Then,
you
have a simpler type system definition which is easier to extend (with
operator
overloading, for instance).
Remark: it does not change much the picture, because you have to find a
subsystem of the simple undecidable system. The difference, is that you can
define the subsystem by some limit to the typing complexity in the
undecidable
system ... This is still far from trivial, but there is a lot of freedom (so
place for research :-).
======================================================================
3) arbitrarily large integers
----------------------------------------------------------------------
J. Scott asked and Jean-Christophe Filliatre answered:
> Hi, is it possible to implement in OCamel arbitrary large integers as
> in Dolphin smalltalk e.g. where e.g. factorial 10000 is evaluatedvery
> fast.
The Num library delivered with ocaml implements arbitrary large
naturals, integers and rationals.
See http://caml.inria.fr/ocaml/htmlman/manual036.html
There are also
- an interface of the GNU MP library, by David Monniaux, at
http://www.di.ens.fr/~monniaux/download/mlgmp-20021123.tar.gz
- The Numerix library by Michel Quercia, at
http://pauillac.inria.fr/~quercia/
======================================================================
Old cwn
----------------------------------------------------------------------
If you happen to miss a cwn, you can send me a message
([email protected]) and I'll mail it to you, or go take a look at
the archive (http://pauillac.inria.fr/~aschmitt/cwn/). If you also wish
to receive it every week by mail, just tell me so.
======================================================================
Alan Schmitt