-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlinear-constraints.mng
3713 lines (3342 loc) · 159 KB
/
linear-constraints.mng
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
% -*- latex -*-
%if style == newcode
module LinearConstraints where
\begin{code}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
import Data.Kind (Constraint)
--import GHC.IO.Unsafe
import GHC.Base
\end{code}
%endif
\documentclass[acmsmall,usenames,dvipsnames,natbib=false,acmthm=false,screen]{acmart}
% \settopmatter{printacmref=false,printfolios=true}
% \usepackage[backend=biber,citestyle=authoryear,style=alphabetic]{biblatex}
\usepackage[backend=biber,datamodel=acmdatamodel, style=acmauthoryear,uniquename=false]{biblatex}
\addbibresource{bibliography.bib}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{subcaption}
\usepackage{hyperref}
\hypersetup{
colorlinks,
linkcolor={red!50!black},
citecolor={blue!50!black},
urlcolor={blue!80!black}
}
\usepackage[plain]{fancyref}
\usepackage[capitalize]{cleveref}
\usepackage{mathpartir}
\usepackage{newunicodechar}
\input{newunicodedefs}
%%%%%%%%%%%%%%%%% ott %%%%%%%%%%%%%%%%%
\usepackage[supertabular,implicitLineBreakHack]{ottalt}
\inputott{ott.tex}
%%%%%%%%%%%%%%%%% /ott %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%% Workaround %%%%%%%%%%%%%%%%%
% This should be handled by the acmclass article, there are a couple
% of issues about
% this. https://github.com/borisveytsman/acmart/issues/271,
% https://github.com/borisveytsman/acmart/issues/327 . Both have been
% merged long ago, and the version of acmart in the shell.nix is from
% 2020.
%% \usepackage{fontspec}
%% \setmainfont{Linux Libertine O}
%% \setsansfont{Linux Biolinum O}
%% \setmonofont{inconsolata}
%%%%%%%%%%%%%%%%% /Workaround %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%% lhs2tex %%%%%%%%%%%%%%%%%
\let\Bbbk\undefined % see https://github.com/kosmikus/lhs2tex/issues/82
%include polycode.fmt
%if style == poly
%format a_i = "\Varid a \ensuremath{_i}"
%format a_j = "\Varid a \ensuremath{_j}"
%format ->. = "⊸"
%format => = "\FatArrow "
%format =>. = "\Lolly "
%format poly_arrow = "\mathop{\to_{\multiplicityfont{m}}}"
%format .<= = "\RLolly"
%format <== = "\RFatArrow"
%format omega = "\omega"
%format IOL = "IO_L"
%format . = "."
%format exists = "\exists"
%format forall = "\forall"
%format pack x = "\packbox" x
%format pack' = "\kpack!"
%format Unique = "\constraintfont{" Linearly "}"
%format unique = linearly
%format constraint (c) = "\constraintfont{" c "}"
%format multiplicity (p) = "\multiplicityfont{" p "}"
%
%format a1
%format a_n
%format an = a_n
%format ^^ = "\,"
%format e1
%format e2
%
%format ! = "!"
%% ^^ this suppresses some space. I think lhs2TeX would otherwise use \mathop
%format spack = "!\kpack"
%format (at n) = "{@}" n
%format phantom x = "\phantom{" x "}"
%endif
%let full = False
%%%%%%%%%%%%%%%%% /lhs2tex %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%% Editing marks %%%%%%%%%%%%%%%%%
% TOGGLE ME to turn off all the commentary:
\InputIfFileExists{no-editing-marks}{
\def\noeditingmarks{}
}
\usepackage{xargs}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
% ^^ Need for pgfsyspdfmark apparently?
\ifx\noeditingmarks\undefined
\setlength{\marginparwidth}{1.2cm} % A size that matches the new PACMPL format
\newcommand{\Red}[1]{{\color{red}{#1}}}
\newcommand{\newaudit}[1]{{\color{blue}{#1}}}
\newcommand{\note}[1]{{\color{blue}{\begin{itemize} \item {#1} \end{itemize}}}}
\newenvironment{alt}{\color{red}}{}
\newcommandx{\jp}[2][1=]{\todo[linecolor=purple,backgroundcolor=purple!25,bordercolor=purple,#1]{#2}}
\newcommandx{\csongor}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=purple,#1]{#2}}
\newcommandx{\rae}[2][1=]{\todo[linecolor=magenta,backgroundcolor=magenta!25,bordercolor=magenta,#1]{RAE: #2}}
\newcommandx{\nw}[2][1=]{\todo[linecolor=green,backgroundcolor=green!25,bordercolor=green,#1]{NW: #2}}
\newcommandx{\unsure}[2][1=]{\todo[linecolor=red,backgroundcolor=red!25,bordercolor=red,#1]{#2}}
\newcommandx{\info}[2][1=]{\todo[linecolor=green,backgroundcolor=green!25,bordercolor=green,#1]{#2}}
\newcommandx{\change}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=blue,#1]{#2}}
\newcommandx{\inconsistent}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=red,#1]{#2}}
\newcommandx{\critical}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=red,#1]{#2}}
\newcommand{\improvement}[1]{\todo[linecolor=pink,backgroundcolor=pink!25,bordercolor=pink]{#1}}
\newcommandx{\resolved}[2][1=]{\todo[linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}} % use this to mark a resolved question
\else
% \newcommand{\Red}[1]{#1}
\newcommand{\Red}[1]{{\color{red}{#1}}}
\newcommand{\newaudit}[1]{#1}
\newcommand{\note}[1]{}
\newenvironment{alt}{}{}
% \renewcommand\todo[2]{}
\newcommand{\unsure}[2][1=]{}
\newcommand{\info}[2][1=]{}
\newcommand{\change}[2]{}
\newcommand{\inconsistent}[2]{}
\newcommand{\critical}[2]{}
\newcommand{\improvement}[1]{}
\newcommand{\resolved}[2]{}
\newcommand{\csongor}[2][1=]{}
\newcommand{\jp}[2][1=]{}
\newcommandx{\rae}[2][1=]{}
\newcommandx{\nw}[2][1=]{}
\fi
%%%%%%%%%%%%%%%%% /Editing marks %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%% Domain-specific macros %%%%%%%%%%%%%%%%%
% Fonts and colours
\newcommand{\constraintcolour}{\color{RoyalBlue}}
\newcommand{\constraintfont}[1]{{\constraintcolour#1}}
\newcommand{\multiplicitycolour}{\color{RoyalBlue}}
\newcommand{\multiplicityfont}[1]{{\multiplicitycolour#1}}
% Utilities
\newcommand{\revop}[1]{\mathop{\reflectbox{\ensuremath{#1}}}}
% Notations
\newcommand{\cscheme}[1]{\mathcal{#1}}
\newcommand{\rlolly}{\mathop{\revop{\multimap}}}
\newcommand{\subst}[2]{[#1]#2}
\newcommand{\sby}[2]{#1 ↦ #2}
% \newcommand{\vdashi}{⊢_{\mathsf{i}}}
\newcommand{\vdashi}{%
\mathrel{%
\vdash\hspace*{-4pt}%
\raisebox{0.9pt}{\scalebox{.66}{\(\blacktriangleright\)}}%
}%
}
\newcommand{\vdashs}{⊢_{\mathsf{s}}}
\newcommand{\vdashsimp}{⊢_{\mathsf{s}}^{\mathsf{a}}}
\newcommand{\scale}{\constraintfont{\cdot}}
%% Constraint notations
\newcommand{\constraintop}[1]{\mathop{\constraintfont{#1}}}
\newcommand{\aand}{\constraintop{\&}}
\DeclareMathOperator*{\bigaand}{\vcenter{\hbox{\Large\&}}}
\newcommand{\lollycirc}{\raisebox{-0.255ex}{\scalebox{1.4}{$\circ$}}}
\newcommand{\Lolly}{\constraintop{=\kern-1.1ex \lollycirc}}
\newcommand{\FatArrow}{\constraintop{\Rightarrow}}
\newcommand{\RLolly}{\mathop{\constraintfont \circledless}}
\newcommand{\RFatArrow}{\constraintop{\rtimes}}
\newcommand{\qtensor}{\constraintop{\otimes}}
%% Desugarer notations
\newcommand{\dsterm}[2]{\llbracket #2 \rrbracket_{#1}}
\newcommand{\dstype}[1]{\llbracket #1 \rrbracket}
\newcommand{\dsevidence}[1]{\llbracket #1 \rrbracket^{\mathbf{ev}}}
% language keywords
\newcommand{\keyword}[1]{\mathbf{#1}}
\newcommand{\klet}{\keyword{let}}
\newcommand{\kcase}{\keyword{case}}
\newcommand{\kwith}{\keyword{with}}
% \newcommand{\packbox}{\square}
\newcommand{\packbox}{\raisebox{-0.08ex}{\scalebox{0.88}{$\square$}}}
\newcommand{\kin}{\keyword{in}}
\newcommand{\kof}{\keyword{of}}
%% Pseudo-keywords for use in text
\newcommand{\kunpack}{\klet\packbox}
% defining grammars
\newcommand{\bnfeq}{\mathrel{\Coloneqq}}
\newcommand{\bnfor}{\mathrel{\mid}}
% theorems
\theoremstyle{acmplain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{property}[theorem]{Property}
\theoremstyle{acmdefinition}
\newtheorem{definition}[theorem]{Definition}
%%%%%%%%%%%%%%%%% /Domain-specific macros %%%%%%%%%%%%%%%%%
\setcopyright{rightsretained}
\acmPrice{}
\acmDOI{10.1145/3547626}
\acmYear{2022}
\copyrightyear{2022}
\acmSubmissionID{icfp22main-p15-p}
\acmJournal{PACMPL}
\acmVolume{6}
\acmNumber{ICFP}
\acmArticle{95}
\acmMonth{8}
% Commented out because of biblatex
% \citestyle{acmauthoryear}
\begin{document}
\title[Linearly Qualified Types: Generic Inference for Capabilities and Uniqueness]{Linearly Qualified Types}
\subtitle{Generic Inference for Capabilities and Uniqueness}
\author{Arnaud Spiwack}
\orcid{0000-0002-5985-2086}
\affiliation{
\institution{Tweag}
\city{Paris}
\country{France}
}
\email{arnaud.spiwack@@tweag.io}
\author{Csongor Kiss}
\orcid{0000-0002-0195-2420}
\affiliation{
\institution{Imperial College London}
\city{London}
\country{United Kingdom}
}
\email{csongor.kiss14@@imperial.ac.uk}
\author{Jean-Philippe Bernardy}
\orcid{0000-0002-8469-5617}
\affiliation{
\institution{University of Gothenburg}
\city{Gothenburg}
\country{Sweden}
}
\email{jean-philippe.bernardy@@gu.se}
\author{Nicolas Wu}
\orcid{0000-0002-4161-985X}
\affiliation{
\institution{Imperial College London}
\city{London}
\country{United Kingdom}
}
\email{n.wu@@imperial.ac.uk}
\author{Richard A.~Eisenberg}
\orcid{0000-0002-7669-9781}
\affiliation{
\institution{Tweag}
\city{Paris}
\country{France}
}
\email{rae@@richarde.dev}
\keywords{GHC, Haskell, linear logic, linear types,
constraints, qualified types, inference}
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10011007.10011006.10011008.10011024</concept_id>
<concept_desc>Software and its engineering~Language features</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011008.10011009.10011012</concept_id>
<concept_desc>Software and its engineering~Functional languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011039</concept_id>
<concept_desc>Software and its engineering~Formal language definitions</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Software and its engineering~Language features}
\ccsdesc[300]{Software and its engineering~Functional languages}
\ccsdesc[300]{Software and its engineering~Formal language definitions}
\begin{abstract}
A linear parameter must be consumed exactly once in the body of its
function. When declaring resources such as file handles and manually
managed memory as linear arguments, a linear type system can verify
that these resources are used safely.
However, writing code with explicit linear arguments requires bureaucracy.
%
This paper presents \emph{linear constraints}, a front-end feature for
linear typing that
decreases the bureaucracy of working with linear types.
%
Linear constraints are implicit linear arguments that are
filled in automatically by the compiler.
%
We present linear constraints as a qualified type system,
together with an inference algorithm which extends
\textsc{ghc}'s existing constraint solver algorithm. Soundness of
linear constraints is ensured by the fact that they desugar into
Linear Haskell.
\end{abstract}
\maketitle
% The full names fit on a line. As per the author instructions, we
% don't need to shorten the authors' names.
% \renewcommand{\shortauthors}{Bernardy, Eisenberg, Kiss, Spiwack, Wu}
\newcommand{\maybesmall}{\small}
\section{Introduction}
\label{sec:introduction}
Linear type systems have seen a renaissance in recent years in
various programming communities. Rust's ownership system guarantees
memory safety for systems programmers, Haskell's \textsc{ghc}~9.0 includes
support for linear types, and even
dependently typed programmers can now use linear types with Idris 2.
All of these systems are vastly different in ergonomics and
scope. Rust uses dedicated syntax and code generation
to support management of resources, while Linear Haskell is a
type system change without any other impact on the compiler, such as in the
code generator or runtime system.\rae{But actually we'd \emph{like} to have
an impact on the runtime system to allow update-in-place.} Linear Haskell
is designed to be general purpose, but
using its linear arguments to emulate Rust's ownership model is a tedious exercise. It
requires
% the compiler doesn't know how to help, requiring
the programmer to carefully thread resource tokens.
To get a sense of the power and the tedium of programming with linear types, consider the
following function:
\begin{code}
read2AndDiscard :: MArray a ->. (Ur a, Ur a)
read2AndDiscard arr0 =
let (arr1, x) = read arr0 0
(arr2, y) = read arr1 1
() = free arr2
in (x, y)
\end{code}
This function reads the first two elements of an array and returns them after
deallocating the array.
Linearity enables the array library to ensure that there is only one reference
to the array, and therefore it can be mutated in-place without violating
referential transparency. Let us stress that this uniqueness property
is an invariant of the array library, not an intrinsic property of
linear functions.
After the array has been freed, it is no longer
possible to read or write to it.
%
Notice that the |read| function consumes the array and returns a
fresh array, to be used in future operations. Operationally, the array remains
the same, but each operation assigns a new name to it, thus facilitating tracking
references statically. Finally, |free| consumes the array without returning a
new one, statically guaranteeing that it can no longer be used.
The values |x| and |y| read from the array are returned; their
types include elements wrapped by the |Ur|
(pronounced ``unrestricted'', and corresponding to the
``!'' operator of \citet{girard-linear-logic}) type, allowing them to be used
arbitrarily many times. This works because |read2AndDiscard| takes a restricted-use array
containing unrestricted elements.
%
In a non-linear language, one would have to forgo referential transparency to
handle mutable operations either by using a monadic interface or allowing
arbitrary effects.
Compare the above function with what one would write in a non-linear, impure
language:
\begin{code}
read2AndDiscard :: MArray a -> (a, a)
read2AndDiscard arr =
let x = read arr 0
y = read arr 1
() = unsafeFree arr
in (x, y)
\end{code}
This non-linear version does not guarantee that there is a unique reference to
the array, so freeing the array is a potentially unsafe operation.
However, it is simpler because there is less bureaucracy to manage: we are
clearly interacting with the \emph{same} array throughout, and this version makes
that apparent.
We see here a clear tension between extra safety and clarity of code---one
we wish, as language designers, to avoid. %% When
%% modelling a handle as a linear resource, the type system must know at all
%% times where it is being consumed, so the file handle is passed around
%% manually, resulting in extra noise.
%
% Reading the non-linear version, it is clear that it keeps a single reference to
% the array.
How can we get the compiler to see that the array is used safely
without explicit threading?
%% Rust introduces the \emph{borrow checker} for this very purpose. % seems out of place when referring to 1999 ideas.
Following well-known ideas~\citep{DBLP:conf/popl/CraryWM99,DBLP:conf/esop/SmithWM00,DBLP:conf/tic/WalkerM00}, our approach is to let arrays be unrestricted, but
associate linear capabilities (such as |constraint(Read)|, |constraint(Write)|) to them.
In fact, we show in this paper that such linear capabilities
are the natural analogue of Haskell's type class
constraints to the setting of linear types.
We call these new constraints \emph{linear constraints}.
Like class constraints,
linear constraints are propagated implicitly by the compiler.
Like linear arguments, they can safely be used to track resources such as arrays
or file handles. Thus, linear constraints are the combination of these two
concepts, which have been studied independently elsewhere
\citep{OutsideIn,LinearHaskell,hh-ll,resource-management-for-ll-proof-search}.
With our extension, we can write a new pure version of |read2AndDiscard| which does
not require explicit threading of the array:
\begin{code}
read2AndDiscard :: constraint ((Read n, Write n)) =>. UArray a n -> (Ur a, Ur a)
read2AndDiscard arr =
let pack x = read arr 0
pack y = read arr 1
pack () = free arr
in (x, y)
\end{code}
The only changes from the impure version are that this version explicitly requires having
read and write access to the array,
and pattern-matching against $\packbox$ (read ``pack'') is necessary in order to access the linear constraint
packed in the result of |read| and |free|. (\Fref{sec:implicit-existentials}
suggests how we can get rid of $\packbox$, too.)
Crucially, the resource representing the ownership of the
array is a linear constraint and is separate from the array itself, which no
longer needs to be threaded manually.
Our contributions are as follows:
\begin{itemize}
\item A system of qualified types that allows a constraint assumption
to be given a multiplicity (linear or unrestricted). Linear assumptions are used precisely
once in the body of a definition
(\Fref{sec:qualified-type-system}). This system supports examples
that have motivated the design of several resource-aware systems,
such as ownership \textit{à la} Rust (\Fref{sec:memory-ownership}), or
capabilities in the style of Mezzo~\cite{mezzo-permissions} or
\textsc{ats}~\cite{AtsLinearViews}; accordingly, our system points
towards a possible unification of these lines of research.
\item Applications of this qualified type system to allow writing
\begin{itemize}
\item resource-aware algorithms without explicit threading (\Fref{sec:memory-ownership}); and
\item functions whose result can only be used linearly (\Fref{sec:Unique-constraint})
\end{itemize}
\item An inference algorithm that respects the multiplicity of
assumptions. We prove that this algorithm is sound with respect to
our type system~(\Fref{sec:type-inference}). It consists of
\begin{itemize}
\item a constraint generation
algorithm~(\cref{sec:constraint-generation}). The language of
generated constraints tracks multiplicities.
\item a solver~(\cref{sec:constraint-solver}) for the generated
constraints, which restricts proof-search algorithms for linear
logic in order to be \emph{guess
free}~\cite[Section~6.4]{OutsideIn}. A guess-free algorithm
ensures that constraint inference is predictable and insensitive
to small changes in the source program; it is necessarily
incomplete.
\end{itemize}
\end{itemize}
%
Our language is given semantics by desugaring into a core language based
on that of \citet{LinearHaskell}.
Our design is intended to work well with other features of Haskell and
\textsc{ghc} extensions. Indeed, we have a prototype implementation (\cref{sec:implementation}).
\section{Background: Linear Haskell}
\label{sec:linear-types}
This section, mostly cribbed from \citet[Section 2.1]{LinearHaskell},
describes our baseline approach, as released in \textsc{ghc}~9.0.
%
Linear Haskell adds a new type of functions,
dubbed \emph{linear functions}, and written |a ⊸ b|.\footnote{The linear function
type and its notation come from linear
logic~\cite{girard-linear-logic}, to which the phrase \emph{linear
types} refers. All the various design of linear typing in the
literature amount to adding such a linear function type, but details
can vary wildly. See~\citet[Section 6]{LinearHaskell} for an analysis
of alternative approaches.} A linear function consumes its
argument exactly once. Linear Haskell defines it as follows: % "thusly" is very rare; let's not summon our inner Shakespeare just yet.
\begin{quote}
% \emph{Meaning of the linear arrow}: %JP: redundant
|f :: a ⊸ b| guarantees that if |(f u)| is consumed exactly once,
then the argument |u| is consumed exactly once.
\end{quote}
To make sense of this statement we need to know what ``consumed exactly once'' means.
Our definition is based on the type of the value concerned:
\begin{definition}[Consume exactly once]~ \label{def:consume}
\begin{itemize}
\item To consume a value of atomic base type (like |Int|) exactly once, just evaluate it.
\item To consume a function exactly once, apply it to one argument, and then consume its result exactly once.
\item To consume a pair exactly once, pattern-match on it, and then consume each component exactly once.
\item In general, to consume a value of an algebraic datatype exactly once, pattern-match on it,
and then consume all its linear components exactly once.
\end{itemize}
\end{definition}
%
\subsection{Multiplicities}
\label{sec:multiplicities}
The usual arrow type |a -> b| can be recovered using |Ur|, as |Ur a ⊸ b|, but Linear
Haskell provides a first-class treatment of |a -> b|, thus ensuring
backwards compatibility with Haskell. In practice, the type-checker
records the \emph{multiplicity} of every introduced variable: \(1\) for linear
arguments and \(ω\) for unrestricted ones. This way, one can give a unified treatment
of both arrow types~\citep{linearity-and-pi-calculus}.
$$
\begin{array}{lcll}
[[{pi}]], [[{rho}]] & \bnfeq & [[{1}]] \bnfor [[{omega}]] & \text{Multiplicities}
\end{array}
$$
We stress that a multiplicity of \(1\) restricts \emph{how the variable can be used}. It does not
restrict \emph{which values can be substituted for it}.
In particular, a linear function cannot assume that it is given the
unique pointer to its argument. For example, if |f :: a ⊸ b|, then
the following is fine:
\begin{code}
g :: a -> (b, b)
g x = (f x, f x)
\end{code}
The type of |g| makes no guarantees about how it uses |x|.
In particular, |g| can pass |x| to |f|.
Pattern matching on a value of type |Ur a| yields a payload of multiplicity
$[[{omega}]]$, even when the scrutinee has multiplicity $[[{1}]]$. In general, given a
multiplicity set, the desired
(sub)structural rules can be obtained by endowing multiplicities with the appropriate
semiring structure~\citep{abel_unified_2020}. In
this paper, we use the same multiplicity structure as Linear Haskell:\footnote{Even though linear Haskell additionally supports multiplicity
polymorphism, we do not support multiplicity polymorphism on
constraint arguments. Linear Haskell takes advantage of multiplicity
polymorphism to avoid duplication of higher-order functions. The
prototypical example is |map :: (a poly_arrow b) -> [a] poly_arrow
[b]|, where |poly_arrow| is the notation for a function arrow of
multiplicity |multiplicity(m)|. First-order functions, on the other
hand, do not need multiplicity polymorphism, because linear functions
can be $\eta$-expanded into unrestricted functions as explained in
\cref{sec:linear-types}. Higher-order functions whose arguments are
themselves constrained functions are rare, so we do not yet see the
need to extend multiplicity polymorphism to apply to constraints.
Futhermore, it is not clear how to extend the constraint solver of
\cref{sec:constraint-solver} to support multiplicity-polymorphic
constraints.}${}^,$\footnote{Here and in the rest of the paper we adopt the convention that
equations defining a function by pattern matching are marked with a
$\left\{\right.$ to their left.}
%
$$
\begin{array}{c@@{\qquad\qquad}c}
\left\{
\begin{array}{lcl}
[[{pi + rho}]] & = & [[{omega}]]
\end{array}
\right.
&
\left\{
\begin{array}{lcl}
[[{1 . pi}]] & = & [[{pi}]] \\
[[{omega . pi}]] & = & [[{omega}]]
\end{array}
\right.
\end{array}
$$
\subsection{Shortcomings of Linear Haskell that We Address}
The |read| function in \cref{sec:introduction} consumes the array it
operates on. Therefore, the same array can no longer be used in
further operations: doing so would result in a type error. To resolve
this, a new name for the same array is produced by each operation.
From the perspective of the programmer, this is unwanted boilerplate.
Minimizing such boilerplate is the main aim of this paper. Our
approach is to let the array be non-linear, and let its
capabilities (\emph{i.e.} having read or write access) be \emph{linear
constraints}. Once these capabilities are consumed, the array can no
longer be read from or written to without triggering a compile time
error.
A further drawback of today's Linear Haskell is that
the programmer cannot restrict how a linear function is used.
For example, suppose we want to use linear types to create
a pure interface to arrays that supports in-place mutation;
the interface is safe only if we guarantee that arrays cannot
be aliased. Because the result of a hypothetical |newArray|
function can be stored in an unrestricted variable (of multiplicity
$[[{omega}]]$), the linearity system cannot prevent its aliasing.
Instead, \citet[Fig.~2]{LinearHaskell} use a continuation-passing
style to enforce non-aliasing.
% In \cref{sec:introduction} and in the rest of the paper, we use pattern matches
% in $\klet$ bindings. By default in Haskell, patterns in $\klet$s are lazy, which means that
% |let (a, b) = p in ()|
% will not actually evaluate the pair. To force evaluation, a strictness annotation can be added:
% |let ^^ !(a, b) = p in ()|.
% Pattern matching in linear $\klet$ bindings must always be strict in Linear Haskell, so writing
% the lazy version would be rejected by the compiler. To simplify the
% presentation, we assume that all patterns in $\klet$ bindings are strict.
% Strict $\klet$ pattern bindings can be desugared into $\kcase$ expressions:
% |case p of (a, b) -> ()|.
\section{Working With Linear Constraints}
\label{sec:what-it-looks-like}
\jp{Why is this here? This current presentation is stuttering. IMO. It should go back somewhere in sec. 4.}
\begin{figure}%
\maybesmall
\centering
\begin{subfigure}{.3\linewidth}%
\noindent%
\begin{code}
phantom ( type constraint(RW n) = constraint((Read n, Write n)) )
new :: Int -> (MArray a ->. Ur r) ->. Ur r
write :: MArray a ->. Int -> a -> MArray a
read :: MArray a ->. Int -> (MArray a, Ur a)
free :: MArray a ->. ()
\end{code}
\caption{Linear Types}
\label{fig:linear-interface}
\end{subfigure}
\hfill
\begin{subfigure}{.55\linewidth}
\begin{code}
type constraint(RW n) = constraint((Read n, Write n))
new :: constraint (Unique) =>. Int -> exists n. UArray a n .<= constraint (RW n)
write :: constraint (RW n) =>. UArray a n -> Int -> a -> () .<= constraint (RW n)
read :: constraint (Read n) =>. UArray a n -> Int -> Ur a .<= constraint (Read n)
free :: constraint (RW n) =>. UArray a n -> ()
\end{code}
\caption{Linear Constraints}
\label{fig:constraints-interface}
\end{subfigure}
\caption{Interfaces for mutable arrays}
\end{figure}
Consider the Haskell function |show|:
\begin{code}
show :: constraint (Show a) => a -> String
\end{code}
In addition to the function arrow |->|, common to all functional
programming languages, the type of this function features a constraint arrow |=>|.
Everything to the
left of a constraint arrow is called a \emph{constraint}, and will be
highlighted in \constraintfont{blue} throughout the paper. Here
|constraint (Show a)| is a
class constraint.
Constraints are handled implicitly by
the typechecker. That is, if we want to |show| the integer |n :: Int| we would write |show
n|, and the typechecker is responsible for proving that |constraint (Show Int)| holds, without
intervention from the programmer.
For our |read2AndDiscard| example, the |constraint((Read n, Write n))| (abbreviated as |constraint(RW n)|)
constraint represents read and write
access to the array tagged with the type variable |n|. (The full \textsc{api} under consideration appears
in \cref{fig:constraints-interface}.)
That is, the constraint |constraint(RW n)|
is provable if and only if the array tagged with |n| is readable and writable.
This constraint is linear: it must be consumed (that is, used as an assumption
in a function call) exactly once.
In order to manage linearity implicitly, this paper introduces a
linear constraint arrow (|=>.|), much like Linear Haskell introduces a linear
function arrow (|->.|). Constraints to the left of a linear constraint
arrow are \emph{linear constraints}.
Using the linear constraint |constraint(RW n)|, we can give
the following type to |free|:
\begin{code}
free :: constraint (RW n) =>. UArray a n -> ()
\end{code}
There are a few things to notice:
\begin{itemize}
\item We have introduced a new type variable |n|. In contrast,
the version in \Cref{fig:linear-interface} without linear
constraints has type |free :: MArray a ->. ()|.
The type variable |n| is a type-level tag used to identify the array.
% Ideally, the linear constraint would refer directly to the
% array value, and have the dependent type |free :: (n :: Array a) -> constraint (RW n) =>. ()|.
% While giving a compile-time name to a function argument is common in
% dependently typed languages such as \textsc{ats}~\cite{ats-lang} or Idris, our
% approach, on the other hand, shows how we can still link a run-time value and a
% compile-time tag without needing any dependent types.
\item The run-time variable representing the array can now be used multiple
times. Instead of restricting the use of this variable,
the linear constraint |constraint(RW n)| controls access to the
array.
\item If we have a single, linear, |constraint (RW n)|
available, then after |free| there will not be any |constraint (RW n)|
left to use, thus preventing the array from being used after freeing.
This is precisely what we were trying to achieve.
\end{itemize}
The above deals with freeing an array and ensuring that it cannot be used afterwards.
However, we still need to explain how a constraint |constraint (RW n)| can come
into scope.
The type of |new| with linear constraints is as follows:
\begin{code}
new :: constraint (Unique) =>. Int -> exists n. UArray a n .<= constraint (RW n)
\end{code}
This type, too, illustrates several new aspects:
\begin{itemize}
\item The |constraint(Unique)| constraint is a linear constraint, though
it takes no type parameter. It restricts the result of |new|
to be used linearly, meaning that any variable that stores the result of |new| must
have multiplicity $[[{1}]]$. |constraint(Unique)| is explained more fully in \Fref{sec:Unique-constraint}.
\item Because |UArray| is now parameterised by a type-level tag |n|, |new| must
return a |UArray| with a fresh such |n|. This is achieved through returning an
existentially-quantified type\footnote{There is a variety of ways that existential types can
be worked into a language. The existentials that we use here may be understood
as a generalisation of those presented by \citet[Chapter
24]{tapl}.
However, \citet{existentials} work out an
approach that makes linear constraints even easier to use, as we
discuss in \Fref{sec:implicit-existentials}. In order to separate
concerns, we do not build our formalism on \citet{existentials},
instead modeling our existentials on the more widely known formulation described by \citet{tapl}.
We additionally freely
omit the |exists a1 ... an.| or |.<= constraint (Q)| parts when they are
empty.
The idea of using existentials to return linear capabilities can be attributed to \citet{DBLP:conf/esop/FluetMA06}.
} packing the type variable |n|. Such types are introduced with the $\packbox$ constructor.
% , which some readers might recognize as $\keyword{pack}$. % redundant with "packing". If there is a specific concept that this refers to, a typeface isn't enough to identify it (explicit reference is needed)
\item Not only do we need a fresh type variable |n|, but we also need to introduce
the linear constraint |constraint(RW n)| for use in subsequent calls to |read| and |free|.
Our existentials also allow packing a constraint, thanks to the |.<=| operator.
\end{itemize}
With all these features working together, we see that |new| returns a non-duplicable
|UArray| tagged with |n|, accessible only when the |constraint(RW n)| constraint is available.
We must also ensure that |read| can both promise to operate only on a readable array
and that the array remains readable afterwards. That is, |read| must both consume
a linear constraint |constraint(Read n)| and also produce a fresh linear constraint
|constraint(Read n)|, as we see in \cref{fig:constraints-interface}, and repeated
here:
\begin{code}
read :: constraint (Read n) =>. UArray a n -> Int -> Ur a .<= constraint (Read n)
\end{code}
%% The fact that existential quantification generates new type-level names
%% is folklore. It's used crucially in the interface of the
%% |ST| monad~\cite{st-monad} and in type-class
%% reflection~\cite{type-class-reflection} (in both of these cases, existential
%% quantification is encoded as rank-2 universal quantification).
%% We
%% shall use it in exactly this way: |openFile| uses an existential
%% quantifier to generate the type-level name of the file
%% handle. Existentially quantified types are paired with a constraint |Q|
%% which we understand as being returned by functions.
% This type has a new symbol, |.<=|, which allows us to pack a produced constraint
% with a returned value. We will see in \cref{sec:arrays} that these produced constraints
% will also sometimes need to come with fresh type variables. Combining these
% ideas, we
% introduce
% a type construction |exists a1 ... an. t .<= constraint(Q)|,
% where |constraint(Q)| is a linear constraint (with the |a1 ... an| in scope) that is
% paired with the type |t|.\footnote{} Such types are introduced with the $\packbox$ constructor.
% Today's Haskell does not have an existential quantifier. However,
% existentially quantified types can
% be encoded as datatypes. For instance, |exists h. Ur (Handle h) .<= constraint (Open h)| can
% be implemented as
% \begin{code}
% data PackHandle where
% Pack :: forall h. constraint (Open h) =>. Handle h -> PackHandle
% \end{code}
% In our implementation (\Fref{sec:implementation}), packed linear constraints
% piggy-back on \textsc{ghc}'s standard \textsc{gadt} syntax. Correspondingly, existential types are
% introduced by a data constructor, which we write as $\packbox$.
% In order to simplify extracting out the payload of an existential, however, we
% introduce a new syntax |let x := f args|: this notation means that the result
% of |f args| is unpacked, putting its payload in |x|. The |:=| notation also
% denotes a \emph{strict} binding, necessary for binding the type variables and
% assuming the constraints carried with |f args|; it can be understood as
% syntactic sugar for a |case| expression.
We have now seen all the ingredients needed to write
the |read2AndDiscard| example as in \cref{sec:introduction}.
\subsection{Minimal Examples}
\label{sec:examples}
To get a sense of how the features that we introduce should behave, we now
look at some simple examples.\jp{This seems either way too late or redundant. How can anyone understand the previous section without already understanding this? I suggest either to 1. move this into the Linear Haskell section (using regular arguments). or 2. delete.} Using constraints to represent
limited resources allows the typechecker to reject certain classes
of ill-behaved programs. Accordingly, the following examples show the
different reasons a program might be rejected.
In what follows, we will be using a constraint |constraint (C)| that is consumed by the |useC|
function.
\begin{code}
useC :: constraint (C) =>. Int
\end{code}
The type of |useC| indicates that it consumes the linear resource |C| exactly once.
\subsubsection{Dithering}
We reject this program:
\begin{code}
dithering :: constraint (C) =>. Bool -> Int
dithering x = if x then useC else 10
\end{code}
The problem with |dithering| is that it does not unconditionally consume |constraint(C)|:
the branch where |x == True| uses the resource |C|,
whereas the other branch does not.
\subsubsection{Neglecting}
Now consider the type of the linear version of |const|:
\begin{spec}
const :: a ->. b -> a
\end{spec}
This function uses its first argument linearly, and ignores the second. Thus,
the the second arrow is unrestricted.
%
One way to improperly use the linear |const| is by neglecting a linear variable:
\begin{code}
neglecting :: constraint (C) =>. Int
neglecting = const 10 useC
\end{code}
The problem with |neglecting| is that, although |useC| is mentioned in this program,
it is never consumed: |const| does not use its second argument.
The constraint |constraint(C)| is not consumed exactly once, and
thus this program is rejected.
%
The rule is that a linear constraint can only be consumed (linearly)
in a linear context. For example,
\begin{code}
notNeglecting :: constraint (C) =>. Int
notNeglecting = const useC 10
\end{code}
is accepted, because the |constraint (C)| constraint is passed on to |useC| which itself
appears as an argument to a linear function (whose result is itself consumed linearly).
\subsubsection{Overusing}
\label{sec:overusing}
Finally, the following program is rejected because it uses |C| twice:
\begin{code}
overusing :: constraint (C) =>. (Int, Int)
overusing = (useC, useC)
\end{code}
%
% However, the
% following version is accepted:
% \begin{code}
% notOverusing :: constraint ((C, C)) =>. (Int, Int)
% notOverusing = (useC, useC)
% \end{code}
% We see here that it is possible to have multiple copies of a given
% constraint.
% Because the consumption of constraints is implicit, when there are
% several possible ways to consume a constraint, the particular order
% chosen will depend on the details of the constraint resolution
% algorithm. We do not want the semantics of programs to depend on this
% order, which would not be at home in a declarative specification of
% the type system. Specifically, we require that the choice of
% given constraint (when there are multiple) cannot influence the
% behavior of the running program. In the domain of class constraints,
% this property is called \emph{coherence}: that only one instance of
% a specific type is in scope. Haskell already has mechanisms to ensure
% coherence~\cite{coherence}, though expert users have discovered ways
% to introduce incoherence\footnote{Kmett's \textsf{reflection} library,
% \url{https://hackage.haskell.org/package/reflection}, both uses incoherence
% to its advantage and also demonstrates techniques to keep its interface
% safe.}. As usual, any introduction of incoherence in the design of
% an \textsc{api} must be carefully considered for possible negative effects;
% the addition of linear constraints does not change this.
% \subsection{Linear I/O}
% \label{sec:linear-io}
% The file-handling example discussed in sections~\ref{sec:linear-types}
% and~\ref{sec:what-it-looks-like} uses a linear version of the |IO| monad, |IOL|.
% Compared to the traditional |IO| monad, the
% type of the monadic operations |>>=| (aka \emph{bind}) and |return| are changed to
% use linear arrows.
% %
% \begin{code}
% (>>=) :: IOL a ->. (a ->. IOL b) ->. IOL b
% return :: a ->. IOL a
% \end{code}
% %
% Bind must be linear because, as explained in the previous section, a linear
% constraint can be consumed in only a linear context. Consider
% the
% following program:
% \begin{code}
% readTwo :: constraint (Open h) =>. Handle h -> IOL (Ur (String, String) .<= constraint (Open h))
% readTwo h = readLine h >>= \case pack' xs ->
% readLine h >>= \case pack' ys ->
% return (pack' (xs, ys))
% \end{code}
% If bind were not linear, the first occurrence of |readLine h| would
% not be able to consume the |constraint (Open h)| constraint
% linearly.
\subsection{Restricting to a Linear Context with |constraint(Unique)|}
\label{sec:Unique-constraint}
A linear function makes a promise about how it is going to use its argument, but
linearity imposes no restrictions on how a function -- or its result -- is going to be used.
The caller may use the linear function's result unrestrictedly. This poses a
challenge for providing a type-safe interface for libraries that rely on having a unique pointer to
some resource, such as safe mutable arrays, because the obvious definition of a
constructor function can immediately be misused, violating the assumption of uniqueness.
%
\begin{code}
new :: Int -> MArray a
bad = let arr = new 5 in (arr, arr)
badToo = Ur (new 5)
\end{code}
%
However, with linear constraints, we can overcome this problem by putting the
special |constraint(Unique)| constraint on |new|:
\begin{code}
new :: constraint(Unique) =>. Int -> MArray a
\end{code}
Suppose we have assumed the |constraint(Unique)| constraint linearly; that is,
we must use the |constraint(Unique)| assumption precisely once. Now, our definition
for |bad| is rejected: either we infer |arr| to have multiplicity~$[[{omega}]]$,
in which case its definition uses |constraint(Unique)| $[[{omega}]]$ times; or
we infer |arr| to have multiplicity~$[[{1}]]$, in which case its use (twice) violates
the linearity restriction. Likewise, the use of |Ur| in |badToo| requires using
the |constraint(Unique)| assumption $[[{omega}]]$ times.
This is promising so far, but several problems remain:
\begin{description}
\item[Duplicating |constraint(Unique)|] What if we want to create multiple
arrays, each of which having a unique pointer? If |constraint(Unique)| is assumed
linearly, then |let arr1 = new 5; arr2 = new 6| will fail, as it uses our
|constraint(Unique)| assumption twice. We thus stipulate that |constraint(Unique)|
must itself be duplicable: from one assumption of |constraint(Unique)|, we
must be able to satisfy any arbitrary fixed number of demands on that constraint.
By ``arbitrary fixed number'', we mean to say that we can duplicate |constraint(Unique)|
a finite number of times, but we may not use an assumption of |constraint(Unique)| with
multiplicity 1 to satisfy |constraint(Unique)| at multiplicity $[[{omega}]]$.
\item[Discarding |constraint(Unique)|] Similarly to allowing
duplication, we must allow discarding, in case a function allocates
no arrays at all. Accordingly, we allow a linear assumption of
|constraint(Unique)| to be accepted even if the constraint is never
used.
\item[Initial assumption of |constraint(Unique)|] For this approach to work,
we must have an assumption of |constraint(Unique)| of multiplicity 1. We can
achieve this via the following primitive:
\begin{code}
unique :: (Unique =>. Ur r) ->. Ur r
\end{code}
The argument to |unique| will be a continuation that assumes |constraint(Unique)|
with multiplicity 1. Because |unique| returns an unrestricted value, no restricted
values from the continuation can escape the scope of the |constraint(Unique)|
assumption. Thus, the continuation has exactly the condition we need: a
linear assumption of |constraint(Unique)|.
\end{description}
The pattern of using a continuation in |unique| mirrors the use
of that technique by \citet[Fig.~2]{LinearHaskell}. But
|unique| is, now, the only place where we need a continuation: once
we have our linear |constraint(Unique)| assumption, we can use it to produce
new values that must be unique.