]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/doc/lablgtk.mgp
- bugfix: typo in XSL patching
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20001129-0.1.0 / doc / lablgtk.mgp
1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 %deffont "code" xfont "itc avant garde gothic-demi-r", tfont "verdana.ttf"
3 %deffont "code-bold" xfont "terminal-bold-r", tfont "verdanab.ttf"
4 %deffont "sans" xfont "helvetica-medium-r", tfont "comic.ttf"
5 %deffont "sans-bold" xfont "helvetica-bold-r", tfont "comicbd.ttf"
6 %deffont "sansit" xfont "helvetica-medium-i", tfont "marlett.ttf"
7 %deffont "title" xfont "times-medium-r", tfont "times.ttf"
8 %deffont "title-bold" xfont "times-bold-r", tfont "timesbd.ttf"
9 %default 1 right, size 2, fore "white", bgrad
10 %default 1 vfont "goth", font "sans-bold", vgap 100
11 %default 2 leftfill, size 8, vgap 60, prefix " ", font "sans"
12 %default 3 size 4, bar "beige", vgap 10
13 %default 4 size 5, fore "white", vgap 20, prefix " "
14 %tab 1  size 5, vgap 40, prefix "  ", icon box "green" 50
15 %tab 2  size 5, vgap 40, prefix "      ", icon arc "yellow" 50
16 %tab 3  size 5, vgap 40, prefix "            ", icon arc "white" 40
17 %tab com1       size 4, prefix "     "
18 %tab com2       size 4, prefix "          "
19 %tab com3       size 4, prefix "             "
20 %tab txt        font "sans", size 5, fore "white", prefix " "
21 %tab vspace     size 2
22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
23 %page
24 %nodefault
25 %size 9, font "title-bold"
26 %fore "beige", back "navyblue", vgap 20
27 %center
28
29
30 A Type System in Action:
31
32 the LablGTK Interface
33
34
35 %size 7, font "title"
36 Jacques Garrigue
37 Kyoto University
38 %size 6, font "code"
39 garrigue@kurims.kyoto-u.ac.jp
40
41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
42 %page
43 2
44 Synopsis
45
46         Objective Label introduction
47 %size 2
48
49         Why GTK+?
50         GTK+/LablGTK structure
51 %size 2
52
53         Low Level
54                 Type encoding with variants
55                 Labeled parameters
56 %size 2
57
58         High Level
59                 Object-orientation
60                 Optional arguments
61                 Polymorphic methods
62 %size 2
63
64         Conclusion
65
66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
67 %page
68 3
69 Objective Label
70
71         Based on Objective Caml
72                 ML syntax and type inference
73                 Class-based object system
74
75         Several extensions
76                 Labeled and optional parameters
77                 Polymorphic variants
78                 Polymorphic methods
79
80         Tools
81                 Type-based browser
82                 GUI and 3D graphics
83
84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
85 %page
86 4
87 Labels and optionals
88
89 %font "code", size 4, prefix "    ", fore "yellow"
90 let rec map fun:f = function
91     [] -> []
92   | x :: l -> f x :: map fun:f l
93 %fore "lightpink"
94 val map : fun:('a -> 'b) -> 'a list -> 'b list
95
96 %pause, fore "yellow", font "code"
97 let f = map [1;2;3]
98 %fore "lightpink"
99 val f : fun:(int -> 'a) -> 'a list
100 %fore "yellow"
101 f fun:(fun x -> 2*x)
102 %fore "lightpink"
103 - : int list = [2; 3; 4]
104
105 %pause, fore "yellow", font "code"
106 let f x ?incr:y [< 1 >] = x + y
107 %fore "lightpink"
108 val f : int -> ?incr:int -> int
109 %fore "yellow"
110 f 1
111 %fore "lightpink"
112 - : int = 2
113
114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
115 %page
116 5
117 Polymorphic variants
118
119
120 %font "code", size 4, prefix "    ", fore "yellow"
121 [`on; `off]
122 %fore "lightpink"
123 - : [> off on] list = [`on; `off]
124
125 %pause, fore "yellow", font "code"
126 `number 1;;
127 %fore "lightpink"
128 - : [> number(int)] = `number 1
129
130 %pause, fore "yellow", font "code"
131 let f = function `on -> 1 | `off -> 0 | `number n -> n
132 %fore "lightpink"
133 val f : [< number(int) off on] -> int
134
135 %pause, fore "yellow", font "code"
136 type t = [on off number(int)]
137
138 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
139 %page
140 6
141 Polymorphic methods
142
143 Not allowed in Objective Caml
144 %size 2
145
146 %font "code", size 4, prefix "    ", fore "yellow"
147 class c = object method m x = x end
148 %fore "red"
149 Some type variables are unbound in this type:
150   class c : object method m : 'a -> 'a end
151 The method m has type 'a -> 'a where 'a is unbound
152
153 %pause, font "sans", size 5, prefix " ", fore "white"
154 Need explicit annotation in O'Labl
155 %size 2
156
157 %font "code", size 4, prefix "    ", fore "yellow"
158 class c = object
159     method m : 'a. 'a -> 'a = fun x -> x
160 end
161 %fore "lightpink"
162 class c : object method m : 'a -> 'a end
163 %fore "yellow"
164 let o = new c
165 %fore "lightpink"
166 val o : c = <obj>
167 %fore "yellow"
168 o#m 1, o#m true
169 %fore "lightpink"
170 - : int * bool = 1, true
171
172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
173 %page
174 7
175 Why GTK+ ?
176
177 Why use the GIMP Tool Kit?
178 %size 3
179
180         Widely used in free software
181
182         Easy to interface
183                 Written in C (QT uses C++)
184                 Memory management
185
186 Drawbacks
187 %size 3
188
189         Design lacks uniformity
190         Extensive use of dynamic typing
191
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
193 %page
194 8
195 GTK+ Structure
196
197 Class hierarchy based on GtkObject
198 %size 2
199
200         Single inheritance
201 &com1 New widgets may redefine methods
202 %size 2
203
204         Dynamically checked
205 &com1 Casting necessay both up and down
206 %size 2
207
208         Developper-side hierarchy
209 &com1 Inheritance is not always meaningful to the user
210 %size 2
211
212 %size 5
213 Signal-based callback mechanism
214 %size 2
215
216         May use multiple callbacks
217 %size 2
218
219         Signals are polymorphic
220
221 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
222 %page
223 9
224 LablGTK structure
225
226 Typed at all levels
227
228         Low-level interface
229 %size 2
230
231                 C stub functions -- typechecked by C
232
233                 ML type declarations -- ML abstract types
234
235         High-level interface
236 %size 2
237
238                 ML class wrappers -- ML concrete types
239
240 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
241 %page
242 10
243 Low Level Interface
244
245 Goals
246
247         Strongly typed interface
248 &com1 heavy use of advanced typing techniques
249
250         Very little ML code
251 &com1 C-stubs and external declarations
252
253         Safe memory management
254 &com1 have the library cooperate with the GC
255
256 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
257 %page
258 11
259 Low level encoding (I)
260
261
262 How to represent widget subtyping in ML?
263
264         Example: buttons' hierarchy
265 %size 2
266
267 %font "code", size 5, prefix "      ", fore "yellow"
268 GtkObject
269     GtkWidget
270         GtkContainer
271             GtkButton
272                 GtkToggleButton
273                     GtkRadioButton
274
275 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
276 %page
277 12
278 Variants as set constraints
279
280
281 Variants can be seen as sets of possible values:
282
283         [tag1 ... tagn] = {tag1,...,tagn}
284
285
286 Polymorphic variants introduce constraints
287
288         \e$B&A\e(B[> tag1 ... tagn] \e$B"N\e(B \e$B&A\e(B \e$B"?\e(B {tag1,...,tagn}
289         \e$B&A\e(B[< tag1 ... tagn] \e$B"N\e(B \e$B&A\e(B \e$B">\e(B {tag1,...,tagn}
290
291 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
292 %page
293 13
294 Encoding hierarchies
295
296 Define an abstract type
297 &vspace
298 %font "code", fore "yellow", size 5
299       type 'a obj
300
301 &txt Use tags to represent properties
302 &vspace
303 %font "code", fore "yellow", size 5
304       type t = [class1 ... classn] obj
305
306 &txt Functions check properties
307 &vspace
308 %font "code", fore "yellow", size 5
309       val f : [> class1 ... classn] obj -> ...
310 &txt
311         Subsumes Haskell type classes
312 &vspace
313         Allows multiple inheritance
314
315 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
316 %page
317 14
318 Low level encoding (II)
319
320 Example: buttons' hierarchy
321 %size 2
322
323 %font "code", size 4, prefix "    ", fore "yellow"
324 type 'a obj
325 type widget = [widget] obj
326 type container = [widget container] obj
327 type button = [widget container button] obj
328 type toggle_button = [widget ... togglebutton] obj
329 type radio_button = [widget ... radiobutton] obj
330 type state_type = [ NORMAL
331      ACTIVE PRELIGHT SELECTED INSENSITIVE ] 
332 val set_state : [> widget] obj -> state_type -> unit
333 val children : [> container] obj -> [widget] obj list
334 val clicked : [> button] obj -> unit
335 val set_group : [> radiobutton] obj -> group -> unit
336
337 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
338 %page
339 15
340 Alternate encoding
341
342 Use only standard ML features
343 %size 2
344
345 %font "code", size 4, prefix "  ", fore "yellow", vgap 50
346 type 'a obj
347 type 'a widget
348 ...
349 type 'a radio
350 type state_type = NORMAL | ACTIVE | ... | INSENSITIVE
351 val set_state : 'a widget obj -> state_type -> unit
352 val children :
353     'a container widget obj -> unit widget obj list
354 val clicked : 'a button container widget obj -> unit
355
356 &txt Weaknesses
357         No multiple inheritance
358         Not very intuitive for the user
359
360 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
361 %page
362 16
363 Low level encoding (III)
364
365 Use of labeled parameters
366 %size 2
367
368 %font "code", size 4, prefix "  ", fore "yellow", vgap 50
369 val adjustment_new :
370     value:float -> lower:float -> upper:float ->
371     step_incr:float -> page_incr:float ->
372     page_size:float -> adjustment obj
373
374 &txt Signals
375 %size 2
376
377 %font "code", size 4, prefix "  ", fore "yellow", vgap 50
378 type ('a,'b) signal =
379     { name: string; marshaller: 'b -> GtkArgv.t -> unit }
380 val connect : 'a obj -> sig:('a,'b) signal ->
381                callback:'b -> ?after:bool -> id
382 val button_clicked : ([> button], unit -> unit) signal
383
384 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
385 %page
386 17
387 High-Level Interface
388
389 Problems with GTK+
390 %size 2
391
392         Name space is scattered
393 &com1 One has to know in which superclass a function is defined
394         Developper oriented design
395 &com1 There is no clear distinction between public and private definitions
396
397 &txt LablGTK design
398 %size 2
399
400         OCaml classes to reunify name space
401         Omit developper-oriented methods
402
403 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
404 %page
405 18
406 High-level classes
407
408 %font "code", size 4, prefix "  ", fore "yellow"
409 class button :
410 %fore "lightgreen"
411   ?label:string ->
412 %fore "lightpink"
413   ?border_width:int ->
414   ?width:int ->
415   ?height:int ->
416 %fore "lightgray"
417   ?packing:(GButton.button -> unit) ->
418   ?show:bool ->
419 %fore "yellow"
420   object
421 %fore "lightgray"
422     method destroy : unit -> unit
423     method as_widget : Gtk.widget obj
424     method misc : GObj.widget_misc
425 %fore "lightpink"
426     method add : #is_widget -> unit
427     method set_border_width : int -> unit
428 %fore "lightgreen"
429     method clicked : unit -> unit
430     method connect : GButton.button_signals
431     method grab_default : unit -> unit
432 %fore "yellow"
433   end
434
435 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
436 %page
437 19
438 High-level features
439
440         Objective Caml classes
441 &com1 allow collecting methods from different modules
442
443         Use optionals in class constructors
444 &com1 makes widget creation much easier
445
446         Polymorphic methods
447 &com1 needed for container widgets
448 %size 2
449
450 %font "code", size 4, fore "yellow", vgap 50
451         method add : 'a. (#is_widget as 'a) -> unit
452
453 %fore "white", font "sans"
454         Polymorphic variants
455 &com1 for C-style enumeration types, avoid name-space dependancies
456
457 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
458 %page
459 20
460 Polymorphic methods (I)
461
462         Instance of first-class polymorphism
463 %size 2
464
465                 first-class polytypes cannot be inferred
466                 they are propagated by the definition flow
467
468         Technically
469 %size 2
470
471                 use polymorphism to track available information
472                 type system excludes derivations based on "guessed" information
473
474
475 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
476 %page
477 21
478 First class polymorphism
479
480 %prefix "            "
481 %image "formula.eps" 512x384
482 %size 2
483
484 %prefix " ", size 5, fore "lightblue"
485   (\e$B&R\e(B1 : \e$B&R\e(B : \e$B&R\e(B2) \e$B"N\e(B \e$B&R\e(B1 = \e$B&H\e(B(\e$B&Q\e(B1(\e$B&R\e(B)) \e$B"J\e(B \e$B&R\e(B2 = \e$B&H\e(B(\e$B&Q\e(B2(\e$B&R\e(B))
486 %fore "white"
487 where \e$B&H\e(B instantiates free variables, and \e$B&Q\e(B1,\e$B&Q\e(B2 rename free labels of \e$B&R\e(B.
488
489 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
490 %page
491 22
492 Polymorphic methods (II)
493
494 Definitions
495 %size 2
496
497 %font "code", size 4, prefix "    ", fore "yellow", vgap 50
498 type is_widget = < as_widget : widget obj >
499 type #is_widget = < as_widget : widget obj; .. >
500 type container =
501     < ... ; add : 'a. (#as_widget as 'a) -> unit; ... >
502
503 %pause
504 &txt Propagation
505 %size 2
506
507 %font "code", size 4, prefix "    ", fore "lightgreen", vgap 50
508 fun (cont : container) -> cont#add widget
509
510 %pause
511 let button = new button in button#add widget
512
513 %pause, fore "red"
514 fun cont -> cont#add widget
515
516 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
517 %page
518 23
519 Programming example
520
521 Hello World
522 %size 2
523
524 %font "code", size 4, prefix "    ", fore "yellow"
525 open GMain
526
527 let window =
528     new GWindow.window border_width: 10
529
530 let button =
531     new GButton.button
532         label: "Hello World" packing: window#add
533
534 let _ =
535   window#connect#destroy callback: Main.quit;
536   button#connect#clicked callback: window#destroy;
537   window#show ();
538   Main.main ()
539
540 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
541 %page
542 24
543 Conclusion
544
545         Results
546 %size 2
547
548                 Could build a strongly typed interface
549
550                 It is easier to use than the C API
551
552                 Makes effective use of extensions to the type system
553
554         Comments
555 %size 2
556
557                 Still difficulties with the Caml object system 
558 &com2 class recursion, method type refinement, etc...