-
Notifications
You must be signed in to change notification settings - Fork 1
/
presentation.html
1033 lines (917 loc) · 42.7 KB
/
presentation.html
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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta name="generator" content="pandoc">
<meta name="author" content="Matt Bovel @LAMP/LARA, EPFL">
<meta name="dcterms.date" content="2022-10-06">
<title>Type-level Programming in Scala</title>
<meta name="apple-mobile-web-app-capable" content="yes">
<meta name="apple-mobile-web-app-status-bar-style" content="black-translucent">
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no, minimal-ui">
<link rel="stylesheet" href="https://unpkg.com/reveal.js@^4//dist/reset.css">
<link rel="stylesheet" href="https://unpkg.com/reveal.js@^4//dist/reveal.css">
<style>
.reveal .sourceCode { /* see #7635 */
overflow: visible;
}
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
span.underline{text-decoration: underline;}
div.column{display: inline-block; vertical-align: top; width: 50%;}
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
ul.task-list{list-style: none;}
</style>
<link rel="stylesheet" href="https://unpkg.com/reveal.js@^4//dist/theme/white.css" id="theme">
<script src="https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.11.1/katex.min.js"></script>
<script>document.addEventListener("DOMContentLoaded", function () {
var mathElements = document.getElementsByClassName("math");
var macros = [];
for (var i = 0; i < mathElements.length; i++) {
var texText = mathElements[i].firstChild;
if (mathElements[i].tagName == "SPAN") {
katex.render(texText.data, mathElements[i], {
displayMode: mathElements[i].classList.contains('display'),
throwOnError: false,
macros: macros,
fleqn: false
});
}}});
</script>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.11.1/katex.min.css" />
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.3.1/styles/atom-one-light.min.css">
<link rel="stylesheet" href="custom.css" />
</head>
<body>
<div class="reveal">
<div class="slides">
<section id="title-slide">
<h1 class="title">Type-level Programming<br/>in Scala</h1>
<p class="author"><a href="mailto:[email protected]">Matt Bovel</a> @<a href="https://www.epfl.ch/labs/lamp/">LAMP</a>/<a href="https://lara.epfl.ch/w/">LARA</a>, <a href="https://www.epfl.ch/fr/">EPFL</a></p>
<p class="date">October 6, 2022</p>
</section>
<section id="TOC">
<nav role="doc-toc">
<h2 id="toc-title">Outline</h2>
<ul>
<li><a href="#/introduction">Introduction</a>
<ul>
<li><a href="#/rockets-explode">Rockets explode</a></li>
<li><a href="#/types-can-help">Types can help</a></li>
<li><a href="#/literal-types">Literal types</a></li>
<li><a href="#/path-dependent-types">Path-dependent types</a></li>
<li> </li>
<li><a href="#/dependent-parameters">Dependent parameters</a></li>
<li><a href="#/dependent-return-types">Dependent return types</a></li>
<li><a href="#/refinement-types">Refinement types</a></li>
<li><a href="#/compile-time-operations">Compile-time operations</a></li>
<li><a href="#/match-types">Match types</a></li>
</ul></li>
<li><a href="#/example-printf">Example: <code>printf</code></a>
<ul>
<li><a href="#/motivation">Motivation</a></li>
<li><a href="#/goal">Goal</a></li>
<li><a href="#/trick-use-parameter-untupling">Trick: use parameter untupling</a></li>
<li><a href="#/signature-of-printf">Signature of <code>printf</code></a></li>
<li><a href="#/code">Code</a></li>
<li><a href="#/related-regsafe">Related: regsafe</a></li>
</ul></li>
<li><a href="#/example-http-routes">Example: HTTP routes</a>
<ul>
<li><a href="#/inspiration-scalatra">Inspiration: Scalatra</a></li>
<li><a href="#/goal-1">Goal</a></li>
<li><a href="#/stringconverter"><code>StringConverter</code></a></li>
<li><a href="#/trick-precise-tuples">Trick: precise tuples</a></li>
<li><a href="#/code-1">Code</a></li>
</ul></li>
<li><a href="#/example-sized-lists">Example: Sized lists</a>
<ul>
<li><a href="#/motivation-1">Motivation</a></li>
<li><a href="#/goal-2">Goal</a></li>
<li><a href="#/code-class-and-type-params">Code (class and type params)</a></li>
<li><a href="#/current-shortcomings">Current shortcomings</a></li>
<li><a href="#/related-why-netflix-s-scala-for-machine-learning">Related: Why Netflix ❤’s Scala for Machine Learning</a></li>
<li><a href="#/related-tf-dotty">Related: <code>tf-dotty</code></a></li>
<li><a href="#/related-towards-typesafe-deep-learning-in-scala">Related: Towards Typesafe Deep Learning in Scala</a></li>
</ul></li>
<li><a href="#/algebraic-laws-for-type-level-operations">Algebraic laws for type-level operations</a>
<ul>
<li><a href="#/ordering">Ordering</a></li>
<li><a href="#/grouping">Grouping</a></li>
<li><a href="#/distribution"><del>Distribution</del></a></li>
<li><a href="#/when-to-normalize">When to normalize?</a></li>
<li><a href="#/example-tf-dotty-with-abstract-dimensions">Example: tf-dotty (with abstract dimensions)</a></li>
<li> </li>
</ul></li>
<li><a href="#/example-sized-lists-contd">Example: Sized lists (cont’d)</a>
<ul>
<li><a href="#/map-method">Map method</a></li>
<li><a href="#/refinement-version">Refinement version</a></li>
<li><a href="#/map-with-refinement">Map with refinement</a></li>
<li><a href="#/helper-method-to-type-nil">Helper method to type Nil</a></li>
<li><a href="#/code-refinement-version">Code (refinement version)</a></li>
</ul></li>
<li><a href="#/precise-inference">Precise inference</a>
<ul>
<li><a href="#/why-not-always-infer-precise-types">Why not always infer precise types?</a></li>
<li><a href="#/problem-1-usability">Problem 1: usability</a></li>
<li><a href="#/problem-2-performance">Problem 2: performance</a></li>
<li><a href="#/problem-3-backward-compatibility">Problem 3: backward compatibility</a></li>
<li> </li>
<li><a href="#/solution-1-separate-term-level-constructs">Solution 1: separate term-level constructs?</a></li>
<li> </li>
<li><a href="#/solution-2-always-precise-and-widen">Solution 2: always precise and widen?</a></li>
<li> </li>
<li><a href="#/solution-3-type-depending-on-the-expected-type">Solution 3: type depending on the expected type</a></li>
<li> </li>
<li><a href="#/solution-4-a-dedicated-inference-mode">Solution 4: a dedicated inference mode?</a></li>
<li> </li>
<li> </li>
<li><a href="#/how-should-precise-inference-propagate">How should precise inference propagate?</a></li>
</ul></li>
</ul>
</nav>
</section>
<section>
<section id="introduction" class="title-slide slide level2">
<h2>Introduction</h2>
</section>
<section id="rockets-explode" class="slide level3">
<h3>Rockets explode</h3>
<div class="float">
<p><img src="images/Explosion_of_first_Ariane_5_flight_June_4_1996.jpg" width="600px" height="395px"></p>
<p><small><a href="https://www.esa.int/ESA_Multimedia/Images/2009/09/Explosion_of_first_Ariane_5_flight_June_4_1996">Explosion of the first Ariane 5 flight, June 4, 1996<br/>© ESA (European Space Agency)</a></small></p>
</div>
<div style="height: 395px; display: flex; align-items: center; justify-content: center;">
<p><span class="math display">
\gdef\tm#1{\textcolor{953800}{\texttt{{#1}}}}
\gdef\tp#1{\textcolor{8250df}{\texttt{{#1}}}}
\tm{x}
</span></p>
</div>
<aside class="notes">
<p><strong>Title Slide</strong></p>
<p>Hello, my name is Matt Bovel and I am a PhD student at EPFL. I am working at LAMP, the lab that builds Scala. It’s just next to the Scala center. And I am co-supervised by Martin Odersky.</p>
<p>My research interests are center around what we can qualify as precise types and so today, I will talk about precise types. More specifically, I will mainly talk about singleton types, refinement types, match types and type-level operations. I will give a pretty general presentation. It’s not very much research-oriented. Instead, after a very brief introduction the presentation will be completely examples-based. I will show practical examples of what we can achieve with the type system of Scala today, and also what we might be able to achieve in the future. So even if you already know everything about these precise types, you might be interested in this later part.</p>
<p><strong>TOC</strong></p>
<p>Ok, before diving into the subject, lets me zoom out for a few slides.</p>
<p><strong>This slide</strong></p>
<p>Writing software is hard. It takes time. And even so, all programs that we use everyday are full of bugs. Software bugs cost the U.S. economy an estimated $59.5 billion annually, or about 0.6 percent of the gross domestic product. So we lose time, money, and in extreme situation, this can lead to catastrophes like the crash of the Ariane 5 rocket—from which you have a picture here.</p>
<p>How can we help? And <em>what</em> can help?</p>
</aside>
</section>
<section id="types-can-help" class="slide level3">
<h3>Types can help</h3>
<div class="float">
<p><img src="images/Artist_s_view_of_the_configuration_of_Ariane_6_using_four_boosters_A64_pillars.jpg" width="600px" height="395px"></p>
<p><small><a href="https://www.esa.int/ESA_Multimedia/Images/2018/06/Artist_s_view_of_the_configuration_of_Ariane_6_using_four_boosters_A643">Artist’s view of the configuration of Ariane 6 using four boosters (A64)<br/>© ESA (European Space Agency)</a></small></p>
</div>
<div style="height: 395px; display: flex; align-items: center; justify-content: center;">
<p><span class="math display">\tm{x}:\tp{Long}</span></p>
</div>
<aside class="notes">
<p>Well, one of the things that can help are <em>type systems</em>. The idea of a type system is to assign a type to each element of a program to make sure that these elements are combined appropriately. If I want to sum two elements and I write <span class="math inline">x + y</span> for example, I want to make sure that <span class="math inline">x</span> and <span class="math inline">y</span> are numbers. If these are something else, then the operation written <code>+</code> might have a complete different meaning or not make sense at all.</p>
<p>Types like strings, integer or boolean are not enough. […]</p>
</aside>
</section>
<section id="literal-types" class="slide level3">
<h3>Literal types</h3>
<p>Type inhabited by a single constant value known at compile-time:</p>
<pre class="scala"><code>val x: 3 = 3
val y: false = false
val z: "monday" = "monday"</code></pre>
<p><small>See <a href="https://docs.scala-lang.org/sips/42.type.html">SIP-23 - literal-based singleton types</a>.</small></p>
</section>
<section id="path-dependent-types" class="slide level3">
<h3>Path-dependent types</h3>
<p>Type inhabited by a single non-necessary-constant term:</p>
<pre class="scala"><code>val a: Int = ???
val b: Int = ???
val c: a.type = a
val d: Int = a // Ok because (a: Int) <: Int</code></pre>
<div class="fragment">
<pre class="scala"><code>val e: a.type = b // Error: found (b: Int)
// but required (a: Int)</code></pre>
</div>
</section>
<section class="slide level3">
<p>It is called <em>path</em>-dependent because it can refer to nested members as well:</p>
<pre class="scala"><code>object Foo:
val x: 3 = 3
summon[Foo.x.type =:= 3]</code></pre>
<div class="fragment">
<p><strong>Note:</strong> instances of the <code>=:=</code> type are generated automatically by the compiler when the left hand-side and the right hand-side are both subtypes of each other. Therefore, <code>summon[X =:= Y]</code> compiles only if <code>X</code> are equivalent <code>Y</code>.</p>
</div>
</section>
<section id="dependent-parameters" class="slide level3">
<h3>Dependent parameters</h3>
<p>Singletons are used to model <em>equality</em> between terms.</p>
<pre class="scala"><code>def same(a: Any, b: a.type) = ???
same(3, 3) // Ok
same(3, 4) // Error</code></pre>
<div class="fragment">
<p>Writing the same function with a type parameter instead has a different meaning. It asks the compiler to find a <code>T</code> such that <code>3 <: T</code> and <code>4 <: T</code> which is satisfiable using <code>T = Int</code>:</p>
<pre class="scala"><code>def same2[T](a: T, b: T) = ???
same2(3, 4) // Ok; T is inferred to be Int</code></pre>
</div>
</section>
<section id="dependent-return-types" class="slide level3">
<h3>Dependent return types</h3>
<pre class="scala"><code>def id(x: Any): x.type = x</code></pre>
</section>
<section id="refinement-types" class="slide level3">
<h3>Refinement types</h3>
<pre class="scala"><code>class Vec:
val size: Int
val v: Vec {val size: 2} = new Vec:
val size: 2 = 2
val vSize: 2 = v.size</code></pre>
</section>
<section id="compile-time-operations" class="slide level3">
<h3>Compile-time operations</h3>
<p>Simple bounded type aliases:</p>
<pre class="scala"><code>infix type +[X <: Int, Y <: Int] <: Int</code></pre>
<div class="fragment">
<p>With special compiler support for constant-folding:</p>
<pre class="scala"><code>import scala.compiletime.ops.int.+
val a: 2 + 2 = 4</code></pre>
<p><small>See <a href="https://github.com/lampepfl/dotty/pull/7628">Add primitive compiletime operations on singleton types #7628</a>.</small></p>
</div>
</section>
<section id="match-types" class="slide level3">
<h3>Match types</h3>
<pre class="scala"><code>type IsEmpty[S <: String] <: Boolean = S match {
case "" => true
case _ => false
}
summon[IsEmpty[""] =:= true]
summon[IsEmpty["hello"] =:= false]</code></pre>
<p><small>See <a href="http://infoscience.epfl.ch/record/290019">Blanvillain, O., Brachthäuser, J., Kjaer, M., & Odersky, M. (2021). Type-Level Programming with Match Types. 70.</a></small></p>
</section></section>
<section>
<section id="example-printf" class="title-slide slide level2">
<h2>Example: <code>printf</code></h2>
</section>
<section id="motivation" class="slide level3">
<h3>Motivation</h3>
<p>Demonstrate a form of dependent typing. In this example, <em>compute</em> the type of a parameter <em>depending</em> on a previous argument.</p>
</section>
<section id="goal" class="slide level3">
<h3>Goal</h3>
<pre class="scala"><code>printf("%s is %d")("Ada", 36) // works
printf("%s is %d")(36, "Ada") // fails</code></pre>
<div class="fragment">
<p>What should be the type of <code>printf</code>?</p>
<pre class="scala"><code>def printf(s: String)(t: ???): Unit = ()</code></pre>
</div>
</section>
<section id="trick-use-parameter-untupling" class="slide level3">
<h3>Trick: use parameter untupling</h3>
<p>New in Scala 3. Automatically wraps function value with <span class="math inline">n > 1</span> parameters in a function type of the form <code>((T_1, ..., T_n)) => U</code></p>
<pre class="scala"><code>def g(f: ((Int, Int)) => Unit) = ()
g({ case (x, y) => () })
g((x, y) => ()) // parameter untupling</code></pre>
<div class="fragment">
<p>Also works for tuple parameters:</p>
<pre class="scala"><code>def g2(x: (Int, Int)) = ()
g2((1, 2))
g2(1, 2)</code></pre>
<p><small>See <a href="https://docs.scala-lang.org/scala3/reference/other-new-features/parameter-untupling.html">Parameter Untupling</a>.</small></p>
</div>
</section>
<section id="signature-of-printf" class="slide level3">
<h3>Signature of <code>printf</code></h3>
<pre class="scala"><code>type ArgTypes[S <: String] <: Tuple = ???
def printf(s: String)(t: ArgTypes[s.type]): Unit = ()</code></pre>
</section>
<section id="code" class="slide level3">
<h3>Code</h3>
<pre class="scala"><code>//> using scala "3.2.0"
//> using options "-Xprint:typer"
import scala.compiletime.ops.int.{+}
import scala.compiletime.ops.string.{CharAt, Length, Substring}
import scala.Tuple._
type ArgTypes[S <: String] <: Tuple = S match
case "" => EmptyTuple
case _ =>
CharAt[S, 0] match
case '%' =>
CharAt[S, 1] match
case 'd' => Int *: ArgTypes[Substring[S, 2, Length[S]]]
case 's' => String *: ArgTypes[Substring[S, 2, Length[S]]]
case _ => ArgTypes[Substring[S, 1, Length[S]]]
def printf(s: String)(t: ArgTypes[s.type]): Unit = ()
def test() =
printf("%s is %d")("Ada", 36) // works
summon[ArgTypes["%s is %d"] =:= (String, Int)]
// printf("%s is %d")(36, "Ada") // fails</code></pre>
<div class="code-source">
<small>Source: <a href="examples/1_printf.scala"><code>examples/1_printf.scala</code></a></small>
</div>
</section>
<section id="related-regsafe" class="slide level3">
<h3>Related: regsafe</h3>
<pre class="scala"><code>import regsafe.Regex
val date = Regex("""(\d{4})-(\d{2})-(\d{2})""")
"2004-01-20" match
case date(y, m, d) =>
s"$y was a good year for PLs."</code></pre>
<p><small>See <a href="https://github.com/OlivierBlanvillain/regsafe">github.com/OlivierBlanvillain/regsafe</a> and <a href="https://2022.ecoop.org/details/scala-2022-papers/1/Type-Safe-Regular-Expressions">Blanvillain, O. (2022). Type-Safe Regular Expressions.</a></small></p>
</section></section>
<section>
<section id="example-http-routes" class="title-slide slide level2">
<h2>Example: HTTP routes</h2>
</section>
<section id="inspiration-scalatra" class="slide level3">
<h3>Inspiration: Scalatra</h3>
<p><a href="https://scalatra.org/guides/2.5/http/routes.html"><img data-src="images/scalatra.png" width="800" /></a></p>
</section>
<section id="goal-1" class="slide level3">
<h3>Goal</h3>
<pre class="scala"><code>Route("user" **: stringValue **: "post" **: intValue **: EmptyTuple)
((userName, postId) => println(userName))</code></pre>
</section>
<section id="stringconverter" class="slide level3">
<h3><code>StringConverter</code></h3>
<p>We present parsers from strings to arbitrary types using a <code>StringConverter</code> class:</p>
<pre class="scala"><code>class StringConverter[T](a: (x: String) => T):
val convert = a</code></pre>
</section>
<section id="trick-precise-tuples" class="slide level3">
<h3>Trick: precise tuples</h3>
<p>By default, type parameters of tuples are widened:</p>
<pre class="scala"><code>val t (Int, Int, Int) = (1, 2, 3)</code></pre>
<p>As a workaround, we define our own precise tuple constructor:</p>
<pre class="scala"><code>extension (a: Any) infix def **:(b: Tuple): a.type *: b.type = a *: b</code></pre>
</section>
<section id="code-1" class="slide level3">
<h3>Code</h3>
<pre class="scala"><code>//> using scala "3.nightly"
//> using options "-Xprint:typer"
import scala.Tuple._
def test() =
Route("user" **: stringValue **: "post" **: intValue **: EmptyTuple)(
(userName, postId) => println(userName)
)
case class Route(partDefs: Tuple)(f: RouteArgTypes[partDefs.type] => Unit)
extension (a: Any) infix def **:(b: Tuple): a.type *: b.type = a *: b
class StringConverter[T](a: (x: String) => T):
val convert = a
val intValue = StringConverter(x => x.toInt)
type IntValue = intValue.type
val stringValue = StringConverter(x => x)
type StringValue = stringValue.type
type RouteArgTypes[R <: Tuple] <: Tuple = R match
case EmptyTuple => EmptyTuple
case h *: t =>
h match
case StringConverter[r] =>
r *: RouteArgTypes[t]
case String =>
RouteArgTypes[t]
@main def test2() =
val matched: (String, Int) = matchRoute(
List("user", "ada", "post", "42"),
"ada" **: stringValue **: "post" **: intValue **: EmptyTuple
)
println(matched)
def matchRoute[R <: Tuple](parts: List[String], partDefs: R): RouteArgTypes[R] =
partDefs match
case _: EmptyTuple => EmptyTuple
case t: (_ *: _) =>
t.head match
case c: StringConverter[_] =>
c.convert(parts.head) *: matchRoute(parts.tail, t.tail)
case _: String =>
matchRoute(parts.tail, t.tail)</code></pre>
<div class="code-source">
<small>Source: <a href="examples/2_routes.scala"><code>examples/2_routes.scala</code></a></small>
</div>
</section></section>
<section>
<section id="example-sized-lists" class="title-slide slide level2">
<h2>Example: Sized lists</h2>
</section>
<section id="motivation-1" class="slide level3">
<h3>Motivation</h3>
<p><strong>For this talk:</strong> demonstrate arithmetic type-level operations.</p>
<p><strong>In general,</strong> applications to:</p>
<ul>
<li>verification of algorithms on lists and tree,</li>
<li>strong typing for machine learning tensors.</li>
</ul>
</section>
<section id="goal-2" class="slide level3">
<h3>Goal</h3>
<p>Keep track of the size of a list in its type.</p>
</section>
<section id="code-class-and-type-params" class="slide level3">
<h3>Code (class and type params)</h3>
<pre class="scala"><code>//> using scala "3.2.0"
//> using options "-Xprint:typer"
import scala.compiletime.ops.int.*
class Vec[Len <: Int, +T]:
def ::[S >: T](x: S): Vec[Len + 1, T] = ???
def tail: Vec[Len - 1, T] = ???
def drop[N <: Int & Singleton](n: N): Vec[Len - N, T] = ???
def head: T = ???
def zip[S](that: Vec[Len, S]): Vec[Len, (T, S)] = ???
def concat[S >: T, ThatLen <: Int](
that: Vec[ThatLen, S]
): Vec[Len + ThatLen, S] = ???
def test() =
val a = Vec[4, String]()
val b = Vec[2, String]()
val c = Vec[5, Int]()
val d = a.concat(b).zip(42 :: c)
val e = a.concat(b).zip(42 :: c)
val f = a.drop(2).concat(b).zip(c.tail)</code></pre>
<div class="code-source">
<small>Source: <a href="examples/3_vec_params_simple.scala"><code>examples/3_vec_params_simple.scala</code></a></small>
</div>
</section>
<section id="current-shortcomings" class="slide level3">
<h3>Current shortcomings</h3>
<p>Cannot reason about operations with non-constant operands.</p>
<pre class="scala"><code>//> using scala "3.2.0"
//> using options "-Xprint:typer"
//> using file "3_vec_params_simple.scala"
def test2() =
val size: Int = ???
val v = Vec[size.type, Int]()
v.zip(42 :: v.tail)
// Error:
// Found: Vec[(size : Int) - (1 : Int) + (1 : Int), Int]
// Required: Vec[(size : Int), Any]</code></pre>
<div class="code-source">
<small>Source: <a href="examples/4_vec_params_shortcomings.scala"><code>examples/4_vec_params_shortcomings.scala</code></a></small>
</div>
</section>
<section id="related-why-netflix-s-scala-for-machine-learning" class="slide level3">
<h3>Related: Why Netflix ❤’s Scala for Machine Learning</h3>
<p><a href="https://youtu.be/BfaBeT0pRe0?t=1155"><img data-src="images/netflix.png" height="500" /></a></p>
</section>
<section id="related-tf-dotty" class="slide level3">
<h3>Related: <code>tf-dotty</code></h3>
<p><a href="https://github.com/MaximeKjaer/tf-dotty"><img data-src="images/tfdotty.png" height="500" /></a></p>
</section>
<section id="related-towards-typesafe-deep-learning-in-scala" class="slide level3">
<h3>Related: Towards Typesafe Deep Learning in Scala</h3>
<p><a href="https://www.youtube.com/watch?v=82A-F14CN2I"><img data-src="images/tensor.png" height="500" /></a></p>
</section></section>
<section>
<section id="algebraic-laws-for-type-level-operations" class="title-slide slide level2">
<h2>Algebraic laws for type-level operations</h2>
</section>
<section id="ordering" class="slide level3">
<h3>Ordering</h3>
<pre class="scala"><code>// Summing x n times is normalized to x * n.
summon[n.type + m.type =:= m.type + n.type]</code></pre>
</section>
<section id="grouping" class="slide level3">
<h3>Grouping</h3>
<pre class="scala"><code>// Summing x n times is normalized to x * n.
summon[2L * m.type =:= m.type + m.type]
summon[2L * m.type + 2L * m.type =:= m.type + 3L * m.type]
summon[2L * m.type * m.type =:= m.type * 2L * m.type]</code></pre>
</section>
<section id="distribution" class="slide level3">
<h3><del>Distribution</del></h3>
<pre class="scala"><code>// Addition is distributed over multiplication.
summon[2L * (m.type + n.type)
=:= 2L * m.type + 2L * n.type]</code></pre>
<p>In the end, we decided not to implement distribution, because it might generate exponentially large types.</p>
</section>
<section id="when-to-normalize" class="slide level3">
<h3>When to normalize?</h3>
<p>Eagerly, or only when comparing types?</p>
<p>Should the user see normalized types?</p>
<pre class="scala"><code>val m: 3 = 3
val n: Int = ???
val v /*:Vec[n.type + 3, String]*/ = Vec[m.type + n.type, String]()</code></pre>
</section>
<section id="example-tf-dotty-with-abstract-dimensions" class="slide level3">
<h3>Example: tf-dotty (with abstract dimensions)</h3>
<pre class="scala"><code>val x: Int = 2
val y: Int = 2
val tensor = tf.zeros(x #: y #: SNil)
val res = tf.reshape(tensor, y #: x #: SNil)</code></pre>
<p><small>See <a href="https://github.com/MaximeKjaer/tf-dotty">github.com/MaximeKjaer/tf-dotty</a>, in particular the <a href="https://github.com/MaximeKjaer/tf-dotty/blob/45af57dd0f60cb2d2fc9cf56f963b6ca4bd32909/modules/tensorflow/src/main/scala/io/kjaer/tensorflow/core/tf.scala#L82-L97">implementation of <code>reshape</code></a>.</small></p>
<p><small>See <a href="http://infoscience.epfl.ch/record/290019">Blanvillain, O., Brachthäuser, J., Kjaer, M., & Odersky, M. (2021). Type-Level Programming with Match Types. 70.</a></small></p>
</section>
<section class="slide level3">
<p>Main ideas behind <code>tf-dotty</code>:</p>
<pre class="scala"><code>//> using scala "3.2.0"
// Inspired by https://github.com/MaximeKjaer/tf-dotty
import scala.compiletime.ops.int.*
sealed trait Shape
infix case class #:[H <: Int & Singleton, T <: Shape](h: H, t: T) extends Shape
object Nil extends Shape
type Nil = Nil.type
def mult[X <: Int, Y <: Int](x: X, y: Y) = (x * y).asInstanceOf[X * Y]
type Size[X <: Shape] <: Int = X match
case Nil => 1
case #:[head, tail] => head * Size[tail]
def size[S <: Shape](s: S): Size[S] = s match
case _: Nil => 1
case cons: #:[head, tail] => mult(cons.h, size(cons.t))
type Reduce[S <: Shape, Axes <: Shape] = ReduceLoop[S, Axes, 0]
type ReduceLoop[S <: Shape, Axes <: Shape, I <: Int] <: Shape = S match
case Nil => Nil
case #:[head, tail] =>
Contains[Axes, I] match
case true => ReduceLoop[tail, Axes, I + 1]
case false => #:[head, ReduceLoop[tail, Axes, I + 1]]
type Contains[S <: Shape, N] = S match
case Nil => false
case #:[N, tail] => true
case #:[head, tail] => Contains[tail, N]
class Tensor[T, S <: Shape]():
def add(t: Tensor[T, S]) = this
def mean[A <: Shape](axes: A): Tensor[T, Reduce[S, A]] =
Tensor[T, Reduce[S, A]]()
def reshape[T, B <: Shape](b: B)(using Size[S] =:= Size[B]): Tensor[T, B] =
Tensor[T, B]()
@main def test() =
val shape = #:(5, #:(6, #:(2, Nil)))
summon[Size[shape.type] <:< 60]
summon[Reduce[shape.type, 0 #: Nil] <:< 6 #: 2 #: Nil]
summon[Reduce[shape.type, 0 #: 2 #: Nil] <:< 6 #: Nil]
summon[Reduce[shape.type, 1 #: 6 #: Nil] <:< 5 #: 2 #: Nil]
val t1 = Tensor[Int, 5 #: 6 #: 2 #: Nil]
val t2 = Tensor[Int, 5 #: 6 #: 2 #: Nil]
val t3 = t1.add(t2)
val t4 = t1.mean(#:(0, #:(2, Nil)))
val t5 = t1.reshape(#:(2, #:(6, #:(5, Nil))))</code></pre>
<div class="code-source">
<small>Source: <a href="examples/5_tf_dotty.scala"><code>examples/5_tf_dotty.scala</code></a></small>
</div>
</section></section>
<section>
<section id="example-sized-lists-contd" class="title-slide slide level2">
<h2>Example: Sized lists (cont’d)</h2>
</section>
<section id="map-method" class="slide level3">
<h3>Map method</h3>
<pre class="scala"><code>//> using scala "3.2.0"
//> using options "-Xprint:typer"
import scala.compiletime.ops.int.*
enum Vec[Len <: Int, +T]:
case Nil extends Vec[0, Nothing]
case NotNil[N <: Int, T]() extends Vec[N, T]
def ::[S >: T](x: S): Vec[Len + 1, T] = ???
def tail: Vec[Len - 1, T] = ???
def head: T = ???
def map[S](f: T => S): Vec[Len, S] =
this match
case Vec.Nil => Vec.Nil
case _ => f(this.head) :: this.tail.map(f)</code></pre>
<div class="code-source">
<small>Source: <a href="examples/6_vec_params.scala"><code>examples/6_vec_params.scala</code></a></small>
</div>
</section>
<section id="refinement-version" class="slide level3">
<h3>Refinement version</h3>
<pre class="scala"><code>class SizedList[+T](private val l: List[T]):
val size = l.size
def ::[S >: T](x: S)
: SizedList[S] {val size: SizedList.this.size.type + 1} = ???
def tail: SizedList[T] {val size: SizedList.this.size.type - 1} = ???
def head: T = ???
val SizedNil = new SizedList(Nil):
override val size: 0 = 0
@main def test =
val xs: SizedList{val size: 2} = "a" :: "b" :: SizedNil</code></pre>
</section>
<section id="map-with-refinement" class="slide level3">
<h3>Map with refinement</h3>
<p>Wrong attempt:</p>
<pre class="scala"><code>def mapWrong[S](f: T => S): SizedList[S] { val size: SizedList.this.size.type } =
if size == 0 then SizedNil
else f(this.head) :: this.tail.map(f)</code></pre>
</section>
<section id="helper-method-to-type-nil" class="slide level3">
<h3>Helper method to type Nil</h3>
<pre class="scala"><code>private def nilOr[T](
f: => T
): SizedList[Nothing] { val size: 0 & SizedList.this.size.type } | T =
if size == 0 then asInstanceOf
else f</code></pre>
</section>
<section id="code-refinement-version" class="slide level3">
<h3>Code (refinement version)</h3>
<pre class="scala"><code>//> using scala "3.2.0"
//> using options "-Xprint:typer"
import scala.compiletime.ops.int.*
class Vec[+T](private val l: List[T]):
val size = l.size
def ::[S >: T](x: S): Vec[S] { val size: SizedList.this.size.type + 1 } = ???
def tail: Vec[T] { val size: SizedList.this.size.type - 1 } = ???
def head: T = ???
def map[S](f: T => S): Vec[S] { val size: SizedList.this.size.type } =
nilOr(f(this.head) :: this.tail.map(f))
def zip[S](
that: Vec[S] { val size: SizedList.this.size.type }
): Vec[(T, S)] { val size: SizedList.this.size.type } =
nilOr((this.head, that.head) :: this.tail.zip(that.tail))
// Manual GDAT-like reasoning
private def nilOr[T](
f: => T
): Vec[Nothing] { val size: 0 & SizedList.this.size.type } | T =
if size == 0 then asInstanceOf
else f
val SizedNil = new SizedList(Nil):
override val size: 0 = 0
/*object SizedNil:
def unapply[T](l: SizedList[T]): Option[SizedList[Nothing] {val size: 0 & l.size.type}] =
if l.size == 0 then Some(l.asInstanceOf)
else None*/</code></pre>
<div class="code-source">
<small>Source: <a href="examples/7_vec_refinements.scala"><code>examples/7_vec_refinements.scala</code></a></small>
</div>
</section></section>
<section>
<section id="precise-inference" class="title-slide slide level2">
<h2>Precise inference</h2>
</section>
<section id="why-not-always-infer-precise-types" class="slide level3">
<h3>Why not always infer precise types?</h3>
</section>
<section id="problem-1-usability" class="slide level3">
<h3>Problem 1: usability</h3>
<div style="width: 70%">
<p>Types are <em>approximations</em> meant to help developers reason about the data they are dealing with.</p>
<p>More often than not, types that are too precise would actually make this harder.</p>
<p>There is no simple solution to know when a more precise type would be useful and when it is not.</p>
</div>
</section>
<section id="problem-2-performance" class="slide level3">
<h3>Problem 2: performance</h3>
<div style="width: 70%">
<p>Keeping all precise types would make the size of types significantly bigger, and with it their memory footprint and the time spent traversing them and and the time spent traversing them .</p>
</div>
</section>
<section id="problem-3-backward-compatibility" class="slide level3">
<h3>Problem 3: backward compatibility</h3>
<div style="width: 70%">
<p>While it might seem at first that subtyping might allow us to always replace the type of a term by one of its subtypes, this is not the case in Scala.</p>
<p>Types in Scala are not only descriptive but also play a central semantic role and impact the <em>elaboration</em> of programs—mainly through implicits search and overloads resolution.</p>
</div>
</section>
<section class="slide level3">
<p>Precising types can for example break previously working implicits search.</p>
<pre class="scala"><code>class A
class B extends A
class Inv[X]
given inv: Inv[A] = Inv()
def f3[N](x: N)(using Inv[N]) = 1984</code></pre>
<div class="fragment">
<pre class="scala"><code>val b = B()
f3(b: A) // works
f3[A](b: B) // works
f3(b: B)(using inv) // works
f3(b: B) // error: no given instance of type Inv[B]</code></pre>
</div>
</section>
<section id="solution-1-separate-term-level-constructs" class="slide level3">
<h3>Solution 1: separate term-level constructs?</h3>
<pre class="scala"><code>extension (a: Any) infix def **:(b: Tuple): a.type *: b.type =
a *: b</code></pre>
<div class="fragment">
<pre class="scala"><code>extension (a: Int) infix def +!(b: Int): a.type + b.type =
(a + b).asInstanceOf[a.type + b.type]</code></pre>
</div>
<div class="fragment">
<pre class="scala"><code>class Person(name: String)
val person: Person {name: "Ada"} =
Person.precise("Ada")</code></pre>
</div>
</section>
<section class="slide level3">
<p><strong>Advantage:</strong> simple, nothing to change in the language.</p>
<p><strong>Drawbacks:</strong></p>
<ul>
<li>verbosity (and not only for API writers),</li>
<li>hard to come up with an elegant syntax.</li>
</ul>
</section>
<section id="solution-2-always-precise-and-widen" class="slide level3">
<h3>Solution 2: always precise and widen?</h3>
<p>By default, singletons and unions are used to type literal, term references and conditionals, but widened during inference:</p>
<pre class="scala"><code>val x /*: Int*/ = 3 /*: 3*/
val y /*: Int*/ = x /*: x.type*/
val z /*: Int*/ = if c then 1 else 2 /*: 1 | 2*/</code></pre>
<p>Could we do the same for constructor types, type-level operations and tuples?</p>
<pre class="scala"><code>val x /*: Person*/ = Person("Ada") /*: Person{val name: "Ada"}*/
val y /*: Int*/ = a + b /*: a.type + b.type*/
val z /*: (Int, Int, Int)*/ = (1, 2, 3) /*: (1,2,3)*/</code></pre>
</section>
<section class="slide level3">
<p><strong>Advantage:</strong></p>
<ul>
<li>similar to an existing mechanism.</li>
</ul>
<p><strong>Drawbacks:</strong></p>
<ul>
<li>verbosity (and not only for API writers),</li>
<li>risky for performance.</li>
</ul>
</section>
<section id="solution-3-type-depending-on-the-expected-type" class="slide level3">
<h3>Solution 3: type depending on the expected type</h3>
<p>By default, the result type of a match is the <abbr title="Least Upper Bound">LUB</abbr> of the result types of the cases</p>
<pre class="scala"><code>val v4 /*: Boolean */ = x match
case _: String => true
case _ => false</code></pre>
<div class="fragment">
<p>But we can also type it as the matching match type if we write it explicitly:</p>
<pre class="scala"><code>type IsString[T <: Any] = T match {
case String => true
case _ => false }
val v5: IsString[x.type] = x match
case _: String => true
case _ => false</code></pre>
</div>
</section>
<section class="slide level3">
<p>Could we do the same for constructor types, type-level operations and tuples?</p>
<p><strong>Advantage:</strong></p>
<ul>
<li>similar to an existing mechanism.</li>
</ul>
<p><strong>Drawbacks:</strong></p>
<ul>
<li>verbosity (and not only for API writers),</li>
<li>complex implementation.</li>
</ul>
</section>
<section id="solution-4-a-dedicated-inference-mode" class="slide level3">
<h3>Solution 4: a dedicated inference mode?</h3>
<p>Proposition: type everything precisely when a value or a function is annotated with the <code>precise</code> keyword.</p>
<pre class="scala"><code>precise def precise() =
val v1 = 1
val v2 = 2 + v1
precise def isString(x: Any) = x match
case _: String => true
case _ => false
val v3 = isString(42)
val v4 = Foo(42)</code></pre>
<p><small>A separate inference mode was first proposed in <a href="https://arxiv.org/abs/2011.07653">“Coming to Terms with Your Choices: An Existential Take on Dependent Types”</a> (with the <code>dependent</code> here). Our implementation follows a similar but weaker semantic. In our case, <code>precise</code> simply instructs the system to type the body of the function “as precisely as possible”, while in the linked technical report it means “as precise as its implementation”.</small></p>
</section>
<section class="slide level3">
<p>Inferred types:</p>
<pre class="scala"><code>precise def precise() =
val v1 /*: (v1: (1: Int))*/ = 1
val v2 /*: (v2: (3: Int))**/ = 2 + v1
precise def isString(x: Any) /*: (x : Any) match {
case String => (true : Boolean)
case Any => (false : Boolean)
}*/ = x match
case _: String => true
case _ => false
val v3 /*: (false: Boolean) */ = isString(42)
val v4 /*: Foo {val x = 42} */ = Foo(42)</code></pre>
</section>
<section class="slide level3">
<p><strong>Advantage:</strong></p>
<ul>
<li>finally less verbose 😻</li>
</ul>
<p><strong>Drawback:</strong></p>
<ul>
<li>brings more complexity to the language.</li>
</ul>
</section>
<section id="how-should-precise-inference-propagate" class="slide level3">
<h3>How should precise inference propagate?</h3>
<pre class="scala"><code>precise def id(x: Int): x.type = x
val n: Int = ???
val y = id(n + 3)</code></pre>
</section></section>
</div>
</div>
<script src="https://unpkg.com/reveal.js@^4//dist/reveal.js"></script>
<!-- reveal.js plugins -->
<script src="https://unpkg.com/reveal.js@^4//plugin/notes/notes.js"></script>
<script src="https://unpkg.com/reveal.js@^4//plugin/search/search.js"></script>
<script src="https://unpkg.com/reveal.js@^4//plugin/zoom/zoom.js"></script>
<script>
// Full list of configuration options available at:
// https://revealjs.com/config/
Reveal.initialize({
// Display controls in the bottom right corner
controls: true,
// Help the user learn the controls by providing hints, for example by
// bouncing the down arrow when they first encounter a vertical slide
controlsTutorial: true,
// Determines where controls appear, "edges" or "bottom-right"
controlsLayout: 'bottom-right',
// Visibility rule for backwards navigation arrows; "faded", "hidden"
// or "visible"
controlsBackArrows: 'faded',
// Display a presentation progress bar
progress: true,
// Display the page number of the current slide
slideNumber: false,
// 'all', 'print', or 'speaker'
showSlideNumber: 'all',
// Add the current slide number to the URL hash so that reloading the
// page/copying the URL will return you to the same slide
hash: true,
// Start with 1 for the hash rather than 0
hashOneBasedIndex: false,
// Flags if we should monitor the hash and change slides accordingly
respondToHashChanges: true,
// Push each slide change to the browser history
history: true,
// Enable keyboard shortcuts for navigation
keyboard: true,
// Enable the slide overview mode
overview: true,
// Disables the default reveal.js slide layout (scaling and centering)
// so that you can use custom CSS layout
disableLayout: false,
// Vertical centering of slides
center: true,
// Enables touch navigation on devices with touch input
touch: true,
// Loop the presentation
loop: false,
// Change the presentation direction to be RTL
rtl: false,
// see https://revealjs.com/vertical-slides/#navigation-mode
navigationMode: 'default',
// Randomizes the order of slides each time the presentation loads
shuffle: false,
// Turns fragments on and off globally
fragments: true,
// Flags whether to include the current fragment in the URL,
// so that reloading brings you to the same fragment position
fragmentInURL: true,
// Flags if the presentation is running in an embedded mode,
// i.e. contained within a limited portion of the screen
embedded: false,
// Flags if we should show a help overlay when the questionmark
// key is pressed
help: true,
// Flags if it should be possible to pause the presentation (blackout)
pause: true,
// Flags if speaker notes should be visible to all viewers
showNotes: false,
// Global override for autoplaying embedded media (null/true/false)
autoPlayMedia: null,
// Global override for preloading lazy-loaded iframes (null/true/false)
preloadIframes: null,
// Number of milliseconds between automatically proceeding to the
// next slide, disabled when set to 0, this value can be overwritten
// by using a data-autoslide attribute on your slides
autoSlide: 0,
// Stop auto-sliding after user input
autoSlideStoppable: true,
// Use this method for navigation when auto-sliding
autoSlideMethod: null,
// Specify the average time in seconds that you think you will spend
// presenting each slide. This is used to show a pacing timer in the
// speaker view
defaultTiming: null,
// Enable slide navigation via mouse wheel
mouseWheel: false,
// The display mode that will be used to show slides
display: 'block',
// Hide cursor if inactive
hideInactiveCursor: true,
// Time before the cursor is hidden (in ms)
hideCursorTime: 5000,
// Opens links in an iframe preview overlay
previewLinks: false,
// Transition style (none/fade/slide/convex/concave/zoom)
transition: 'none',
// Transition speed (default/fast/slow)
transitionSpeed: 'default',