From 4362020a2b8c0284c1e668e8e61a415a9712275f Mon Sep 17 00:00:00 2001 From: regnat Date: Mon, 21 Aug 2017 17:12:00 +0200 Subject: [PATCH] Final tweaks --- appendix/nix-light-semantics.tex | 2 +- context/nix/general-presentation.md | 8 ++-- context/nix/syntax-and-semantics.md | 21 +++++---- context/set-theoretic-types.md | 9 ++-- contributions.md | 73 ----------------------------- implem/cduce.md | 7 ++- implem/extensions.md | 12 ++--- main.md | 2 +- main.tex | 1 + nix-light/compilation.md | 5 +- nix-light/description.md | 12 ++--- nix-light/motivation.md | 9 ++-- references.bib | 9 ++++ synthesis.md | 27 +++++++---- typing/lambda-calculus.md | 6 +-- typing/lists.md | 2 +- typing/records.md | 36 +++++++++----- typing/types.md | 12 +++-- 18 files changed, 106 insertions(+), 147 deletions(-) delete mode 100644 contributions.md diff --git a/appendix/nix-light-semantics.tex b/appendix/nix-light-semantics.tex index 6961d12..959057e 100644 --- a/appendix/nix-light-semantics.tex +++ b/appendix/nix-light-semantics.tex @@ -36,7 +36,7 @@ °{ x = e; $\cdots$ }.x° &\leadsto °e° \\ °{ x = e; $\cdots$ }.x or e'° &\leadsto °e° \\ °{ $x_1$ = $e_1$; $\cdots$; $x_n$ = $e_n$ }.x or e'° &\leadsto °e'° - \quad if $x \notin \{ $x_1$, \cdots, $x_n$ \}$ \\ + \quad if $x \notin \{ x_1, \cdots, x_n \}$ \\ °Head(Cons($e_1$, $e_2$))° &\leadsto °$e_1$° \\ °Tail(Cons($e_1$, $e_2$))° &\leadsto °$e_2$° \\ °e : τ° &\leadsto °e° diff --git a/context/nix/general-presentation.md b/context/nix/general-presentation.md index c5dd93d..7900285 100644 --- a/context/nix/general-presentation.md +++ b/context/nix/general-presentation.md @@ -48,12 +48,12 @@ aspects: - \texttt{nixpkgs}, the Nix package collection is today several hundreds of thousands of lines of code, with some really complex parts. The absence of typing makes every non-trivial modification particularly - complicated and dangerous. + complicated and dangerous; - Partly because of its very fast grow, the project suffers from a huge lack of documentation. In particular, a lot of complex internal abstractions are used but not documented at all. - A type-system would reduce the impact of this problem. + A type-system would reduce the impact of this problem; - Nix explores some really interesting ideas by applying to system management some principles coming from programing. Adding a type-system to it opens new @@ -66,11 +66,11 @@ The language presents many characteristics that constrain a type-system for it: - It is possible to know at runtime the type of a value. This functionality is used a lot in practice and requires a notion of union types to be useful, as - we will see. + we will see; - The fields of the records may have dynamically defined labels (i.e., labels which are defined as the result of the evaluation of an arbitrary expression - − provided it evaluates to a string). + − provided it evaluates to a string); - The language has been existing for ten years without a type-system. This naturally led to the introduction of several programing patterns are hard to diff --git a/context/nix/syntax-and-semantics.md b/context/nix/syntax-and-semantics.md index 7aca39d..9d8f53b 100644 --- a/context/nix/syntax-and-semantics.md +++ b/context/nix/syntax-and-semantics.md @@ -13,9 +13,9 @@ This language is a lazily-evaluated lambda calculus, with some additions, namely: - Constants, let-bindings (always recursive), some (hardcoded) infix operators - and `if` constructs. + and `if` constructs; -- Lists, constructed by the `[ $\cdots$ ]` syntax. +- Lists, constructed by the `[ $\cdots$ ]` syntax; - Records, defined by the `{ ; ... ; }` syntax. The labels of record fields may be dynamically defined as the result of @@ -26,7 +26,7 @@ namely: Records may be recursively defined (using the `rec` keyword), in which case, fields may depend one from another. For example, the expression `rec { x = 1; y = x; }` is equivalent to - `{ x = 1; y = 1; }`. + `{ x = 1; y = 1; }`; - A syntax for accessing record fields, of the form `.`. Like for the definition of record litterals, the field names may be arbitrary @@ -37,22 +37,25 @@ namely: For example, `{ x = { y = 1; }; }.x.y` evaluates as `1`, `{ x = { y = 1; }; }.x.z or 2` evaluates as `2` and `{ x = { y = 2; }; }.y` - raises an error. + raises an error; -- Lambda-abstractions can be defined with patterns. +- Lambda-abstractions, that can be defined with patterns. Patterns only exists for records and are of the form `{ , $\cdots$, }` or - `{ , $\cdots$, , "..." }`, with the + `{ , $\cdots$, , .. }`, with the `` construct of the form `` or ` ? ` (the latter specifying a default value in case the field is absent). + The `..` at the end of the pattern indicates that this pattern is *open*, + which means that it will accept a record with more fields than the ones that + are written. Contrary to most languages where the capture variable may be different from the name of the field (for example in OCaml, a pattern matching e record would be of the form `{ x = fieldname1; y = fieldname2; }` and the pattern `{ x; y }` is nothing but syntactic sugar for `{ x = x; y = y }`), Nix requires the name of the capture variable to be the same as the name of - the field. + the field; - Type annotations (absent in the actual language but added for this work). These annotations have been added as they are required by the typechecker. @@ -60,7 +63,7 @@ namely: the gradual types (noted `<τ>`). The meaning of the types will be presented in \Cref{sec:typing}. - The constructions `` and `<ρ>` represents type regular exepressions + The constructions `` and `<ρ>` represents type regular expressions which will be presented in \Cref{typing::structures::listes}. The construction `` (for a type) represents singleton types: for @@ -69,7 +72,7 @@ namely: In addition to these syntactic constructions, a lot of the expressiveness of the language resides in some predefined functions. For example, some functions perform some advanced operations on records, like -the `attNames` function, which when applied to a record returns the list of the +the `attrNames` function, which when applied to a record returns the list of the labels of this record (as strings). Another important class of functions is the set of functions that discriminate over a type, that is functions such as `isInt`, `isString`, `isBool`, and so on, diff --git a/context/set-theoretic-types.md b/context/set-theoretic-types.md index 04e70cb..30c976c 100644 --- a/context/set-theoretic-types.md +++ b/context/set-theoretic-types.md @@ -17,14 +17,13 @@ type-system. In particular : `λx. if isInt x then x==1 else not x` can be typed (with type `Int $\vee$ Bool -> Bool`). -Several existing type-systems already try to satisfy these requirements. -The most well-known one is probably the type-system of Typed Racket (@FH08), which +Several existing type-systems already try to satisfy these requirements. The +most well-known one is probably the type-system of Typed Racket (@FH08), which already implements at an industrial level most of what is needed in the context of the Scheme language. -The approach we choose here is based on the work of Alain Frisch and Giuseppe -Castagna on set-theoretic types (@Fri04 and @Cas15), with extensions brought by -Kim Nguyễn (@phdkim) and Giuseppe Castagna and Victor Lanvin (@CL17). +The approach we choose here is based on the work of @Fri04 and @Cas15 on +set-theoretic types, with extensions brought by @phdkim and @CL17. The system is based on a set-theoretic interpretation of types as a sets of values, which provides a natural interpretation for union, intersection or diff --git a/contributions.md b/contributions.md deleted file mode 100644 index d4f56ee..0000000 --- a/contributions.md +++ /dev/null @@ -1,73 +0,0 @@ -This works makes several technical contributions. In particular: - -- the compilation of if constructs into typecases to account for occurrence - typing, - -- the addition of bidirectional typing to set-theoretic type-systems. - In particular, a technique to propagate type informations through the - syntactic tree (and in particular through lambdas thanks to the $\mathcal{A}$ - function which decomposes a function type into the set of its toplevel - arrows), - -- a new way of typing records with dynamic labels extending the formalism of - @Fri04 with static records, - -- an extension of the gradual type-system of @CL17 with records, - -- \vdots - - -But besides these technical aspects, the most important contribution of -this work is, by far, that it brings together and integrates into a unique -system five different typing techniques that hitherto lived in -isolation one from the other, that is: - -1. gradual typing - -2. occurrence typing - -3. set-theoretic types - -4. bidirectional typing techniques - -5. dynamic records - -The important distinctive aspect that characterizes our study is that -this integration was studied not for some *ad hoc* toy/idealized -academic language, but for an existing programming language with an important -community of programmers, with thousands of lines of existing code, -and, last but surely not least, which was designed not having types in -mind, far from that. The choice of the language dictated the adoption -of the five characteristics above: gradual typing was the solution we -chose to inject the flexibility needed to accept already existing code -that would not fit standard static typing discipline; occurrence typing was -needed to account for common usage patterns in which programmers use -distinct piece of codes according to dynamic type-checks of some -expressions; set-theoretic types were chosen because they provide both -intersection types (we need them to precisely type overloaded -functions which, typically, appear when occurrence typing is -performed on a parameter of a function) and union types (we need them to -give maximum flexibility for occurrence typing, which can typed by -calculating the least upper bound of the different alternatives); -bidirectional typing was adopted to allow the programmer to specify -overloaded types for functions via a simple explicit annotation, -without resorting to the heavy annotation that characterise functions -in CDuce; dynamic records were forced on us by the insanely great -flexibility that Nix designer have decided to give to their language. - -Choosing an existing language also forced us to privilege practical -aspects over theoretical ones − with the drawbacks and the advantages that this -choice implies. The main drawback is that we gave up having a system that is -formally proved to be sound. For instance, we could have designed a type system -in which record field selections are statically ensured always to succeed, but -this would have meant to reject nearly all programs that use dynamic labels -(which are many); likewise, gradual typing is used to shunt the type system -rather than to insert explicit casts that dynamically check the soundness of -programs as @ST06 do: in that sense we completely adhere to the philosophy of -Typed Racked that wants to annotate and document existing code but not modify -(or, worse, reject) any of it. -The implementation of this type system is the most important practical -contribution of this work. To this and to the design of how practically -integrate types in Nix we dedicated an important part of the time spent on this -internship. - diff --git a/implem/cduce.md b/implem/cduce.md index 3d9bdf3..243c630 100644 --- a/implem/cduce.md +++ b/implem/cduce.md @@ -1,5 +1,4 @@ -\newcommand{\cduce}{CDuce} -Instead of implementing our own implementation of types and of the subtyping +Instead of working our own implementation of types and of the subtyping algorithm, we reused those of the implementation of the \cduce{} language[@Ball03]. @@ -8,8 +7,8 @@ features a type-system based on the set-theoretic types of @Fri04 (on which this work is itself based). Although its type-system is obviously not the same as the one presented here, its types form a supertype of ours (with the exception of the gradual type -which is absent in \cduce{} but may be encoded as a distinguished type constant), -so we could reuse its representation. +which is absent in \cduce{} but may be encoded), so we could reuse its +representation. We also wanted to reuse its subtyping algorithm (since implementing it would have taken way too much time), but this was more difficult, as it implements a diff --git a/implem/extensions.md b/implem/extensions.md index a16028d..d8ed992 100644 --- a/implem/extensions.md +++ b/implem/extensions.md @@ -45,9 +45,9 @@ will not. It is possible to get more flexibility by recognizing that the notion of a predicate on a type `t` is a function of type `(t -> true) AND ($\lnot$t -> false)`. -We can thus modify the Nix-light language by replacing the typecase and -replacing it with an if construct, and replace the typecase rules by the -following ones: +We can thus modify the Nix-light language by removing the typecase and +replacing it with an if construct, and replace the associated typing rules by +the following ones: \begin{mathpar} \inferrule{ @@ -113,10 +113,10 @@ Otherwise, if its arguments evaluates to a value `v`, it evaluates to As long as we do not try to track exceptions, a reasonable rule for this is: \begin{displaymath} - \inferrule{Γ \vdash e : τ}{% - Γ \vdash \operatorname{tryEval}(e) : \{ success = \text{Bool}; value = \text{Bool} \vee τ \}} + \inferrule{Γ \tIC e : τ}{% + Γ \tIC \operatorname{tryEval}(e) : \{ success = \text{Bool}; value = \text{false} \vee τ \}} \end{displaymath} (note that in presence of polymorphism, it would have been enough to type `tryEval` as a function of type -`$\forall \alpha$. $\alpha$ -> { success = Bool; value = $\alpha$ | Bool}`). +`$\forall \alpha$. $\alpha$ -> { success = Bool; value = $\alpha$ $\vee$ false}`). diff --git a/main.md b/main.md index f49b2e3..8c57bbc 100644 --- a/main.md +++ b/main.md @@ -90,7 +90,7 @@ We now extends our core calculus with the two builtins data structures of Nix \label{sec:implementation} \input{out/generated/implem/intro.tex} -## CDuce and subtyping +## \cduce{} and subtyping \input{out/generated/implem/cduce.tex} ## Adaptation of the type-system diff --git a/main.tex b/main.tex index 07a3bd9..d7f1e19 100644 --- a/main.tex +++ b/main.tex @@ -87,6 +87,7 @@ \catcode`λ=13 \catcode`ρ=13 \catcode`Γ=13 +\newcommand{\cduce}{$\mathbb{C}$Duce} \newcommand{λ}{\ensuremath{\lambda}} \newcommand{σ}{\ensuremath{\sigma}} \newcommand{τ}{\ensuremath{\tau}} diff --git a/nix-light/compilation.md b/nix-light/compilation.md index 759f082..2e009a7 100644 --- a/nix-light/compilation.md +++ b/nix-light/compilation.md @@ -47,7 +47,7 @@ The compilation of records is slightly complex, for two reasons: For example, the record `{ DOLLAR{e1}.x = 1; DOLLAR{e2}.y = 2; }` may be either of the form `{ z = { x = 1; y = 2; }; }` or `{ z1 = { x = 1; }; z2 = { x = 2; }; }` depending on whether `e1` and `e2` - evaluate to the same value or not. + evaluate to the same value `z` or not. It is then impossible to compile this exactly. The solution we use here is to always assume that they are different. @@ -90,4 +90,5 @@ be compiled to the Nix-light expression `(x = x tin Int) ? x : ((x = x tin Bool) ? x : false)`, on which we will be able to perform occurrence typing for `x`. This pre-processing can be done for any boolean combination of expressions in -the `if` clause thanks to the rewriting rules of \Cref{nix-light::preprocessing} +the `if` clause thanks to the rewriting rules of +\Cref{nix-light::preprocessing}. diff --git a/nix-light/description.md b/nix-light/description.md index 706dea6..529870f 100644 --- a/nix-light/description.md +++ b/nix-light/description.md @@ -6,8 +6,8 @@ which require a special treatment from the typechecker. The differences are: - The `if` construct is replaced by the more general "typecase" construct of the - form `(x = e0 tin t) ? e1 : e2` (which evaluates to `e1` if `e0` evaluates to - a value of type `t` and to `e2` otherwise). + form `(x = e0 tin t) ? e1 : e2` (which evaluates to `e1[x:=e0]` if `e0` + evaluates to a value of type `t` and to `e2[x:=e0]` otherwise). The general case `if e0 then e1 else e2` will be compiled to `(x = (e0 : Bool) tin true) ? e1 : e2` (where `x` is a fresh variable), whereas particular cases such as `if isInt x then e1 else e2` will be compiled @@ -52,7 +52,7 @@ pairwise distinct. ##### Pattern-matching Pattern-matching in Nix-light has a rather classical semantic for a lazy -language, with the simplification that as patterns are not recursive, the +language, with the simplification that, as patterns are not recursive, the argument is either non-evaluated at all, or evaluated in head normal form. \newcommand{\var}{\mathcal{V}} @@ -62,11 +62,11 @@ $\var(r)$) as $\var(x) = \var(x:τ) = x$. We extend this defintion to a record pattern field `l` (of the form `r` or `r?c` where `c` is a constant) by stating that $\var(r ? c) = \var(r)$. In what follows, `l` denotes a record-pattern field of the form `r` or `r?c` -(where `c` is a constant). +(where `c` is a constant and `r` a variable pattern). For a pattern `p` and a value `v` (resp. an expression `e`), we note -$\sfrac{p}{v}$ the substitution generated by the matching of `v` (resp. `e`) -against `p`. +$\sfrac{p}{v}$ (resp. $\sfrac{p}{e}$) the substitution generated by the +matching of `v` (resp. `e`) against `p`. It is defined in \Cref{nix-light::pattern-matching}. The basic idea from which all the rules derive is that the matching of any expression `e` against a variable pattern will produce the substitution `x := diff --git a/nix-light/motivation.md b/nix-light/motivation.md index 81a5d64..533e6b4 100644 --- a/nix-light/motivation.md +++ b/nix-light/motivation.md @@ -18,13 +18,14 @@ the type `{ x = Int }`. Thanks to the use of overloaded functions, we can even give a useful typing to more complex applications. If `f` is of type `(Int -> Bool) AND (String -> String)` (i.e., `f` is an overloaded function -which is a function of type `Int -> Bool` and as a function of type +which is both a function of type `Int -> Bool` and a function of type `String -> String`), we can give the type `{ x = Bool; y = String }` to the expression `mapAttr f { x = 1; y = "foo"; }`. But these two expressions corresponds to two incompatibles types for `mapAttr` (namely `(Int -> Int) -> { x = Int } -> { x = Int }` and -`(Int -> Bool AND String -> String) -> { x = Int; y = String } -> { x = Bool; y = String }`. +`(Int -> Bool AND String -> String) -> { x = Int; y = String } -> { x = Bool; y = String }`). Because of this, it is quite hard to reason on Nix. -Thus, we decided not to work on Nix itself, but on a simpler language, to which -Nix (or at least a large enough subset of it) can be compiled. +Thus, we decided not to work on Nix itself, but on a simpler language, +Nix-light, to which Nix (or at least a large enough subset of it) can be +compiled. diff --git a/references.bib b/references.bib index 5b9f545..270246c 100644 --- a/references.bib +++ b/references.bib @@ -86,6 +86,15 @@ month = {September} year = {1998} } +@InProceedings{DN13, + author = {Joshua Dunfield and Neelakantan R. Krishnaswami}, + title = {Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism}, + booktitle = {Int'l Conf. Functional Programming}, + month = sep, + year = {2013}, + note = {\url{arXiv:1306.6032 [cs.PL]}} +} + @phdthesis{phdeelco, author={Eelco Dolstra}, title={The Purely Functional Software Deployment Model}, diff --git a/synthesis.md b/synthesis.md index de432be..43587fe 100644 --- a/synthesis.md +++ b/synthesis.md @@ -5,8 +5,8 @@ apply concepts coming from the world of programing languages (functional ones in particular) to package management. This approach solves in a very elegant way many problems encountered by conventional package managers (Apt, Pacman, Yum, \ldots). -The state of a machine is (apart from some irreducible mutable state) -entirely described by the result of the evaluation of an expression in a +The state of a machine managed by Nix is (apart from some irreducible mutable +state) entirely described by the result of the evaluation of an expression in a (purely functional) specialized language also called Nix. ## Problem studied {-} @@ -33,20 +33,20 @@ This works makes several technical contributions. In particular: occurrence typing, - an improved definition of bidirectional typing for set-theoretic type-systems. In particular, a technique to propagate type informations through the - syntactic tree (and in particular through lambdas) + syntactic tree (especially through lambdas), - an extension of the gradual type-system of @CL17 with records, -- a new way of typing records with dynamic labels that extends the formalism of - @Fri04 with static records. +- a new way of typing records with dynamic labels that extends the formalism + established by @Fri04 in the case of static records. But besides these technical aspects, the most important contribution of this work is, by far, that it brings together and integrates into a unique system five different typing techniques that hitherto lived in isolation one from the other, that is: -1. gradual typing [@ST06][@CL17] +1. gradual typing [@ST06; @CL17] 2. occurrence typing [@FH08] 3. set-theoretic types [@Fri04] -4. bidirectional typing techniques [@HP98] +4. bidirectional typing techniques [@HP98; @DN13] 5. dynamic records The important distinctive aspect that characterizes our study is that this @@ -67,9 +67,9 @@ flexibility to occurrence typing, which can typed by calculating the least upper bound of the different alternatives); *bidirectional typing* was adopted to allow the programmer to specify overloaded types for functions via a simple explicit annotation, without resorting to the heavy annotation that -characterise functions in CDuce; *dynamic records* were forced on us by the -insanely great flexibility that Nix designers have decided to give to their -language. +characterise functions in most similar type-systems; *dynamic records* were +forced on us by the insanely great flexibility that Nix designers have decided +to give to their language. Choosing an existing language also forced us to privilege practical aspects over theoretical ones − with the drawbacks and the advantages that this @@ -117,3 +117,10 @@ An annoying lack that would deserve to be filled is the absence of polymorphism in the type system. This was essentially due to the fact that the gradual typing system of @CL17 was set in a monomorphic type-system. However, a recent extension by @Call18 adds polymorphism to this system, which may be used here. + +#### Note on the language {-} + +A large part of this document is intended to be presented in the conference +\ 2018^[http://2018.programming-conference.org/], which is +why it is written in English. + diff --git a/typing/lambda-calculus.md b/typing/lambda-calculus.md index 13ae17a..58a9b44 100644 --- a/typing/lambda-calculus.md +++ b/typing/lambda-calculus.md @@ -6,7 +6,7 @@ consisting of a lambda-calculus with typecase (i.e., we exclude lists and records and all the related operations which will be dealt with in \Cref{typing::structures}). -The type-system is divided into two parts: an "inference" system and a "check" +The type-system is divided into two parts: an *inference* system and a *check* one. The first one corresponds to classical bottom-up type inference while the second one is a top-down system which does not do any inference but only tries @@ -128,8 +128,8 @@ then $\A(\tau)$ is defined as where $\sqcup$ is itself defined as \begin{displaymath} - \{ σ_i \rightarrow \tau_i \| i \in I \} \sqcup \{ σ_j \rightarrow \tau_j \| j \in J \} = - \{ (σ_i \wedge σ_j) \rightarrow (\tau_i \vee \tau_j) \| i \in I, j \in J \} + \{ σ_i \rightarrow \tau_i | i \in I \} \sqcup \{ σ_j \rightarrow \tau_j | j \in J \} = + \{ (σ_i \wedge σ_j) \rightarrow (\tau_i \vee \tau_j) | i \in I, j \in J \} \end{displaymath} @Fri04 shows that $τ$ can always be expressed in the form of the diff --git a/typing/lists.md b/typing/lists.md index 19d7184..b684442 100644 --- a/typing/lists.md +++ b/typing/lists.md @@ -9,7 +9,7 @@ types]. The regular expressions `ρ` describe the types of the elements of the list the same way as a textual regular expression describes a family of characters sequence. -For example, `[ Int* ]` is the type of (possibly empty )lists whose elements +For example, `[ Int* ]` is the type of (possibly empty) lists whose elements are of type `Int`, `[ Bool Int* ]` the type of lists containing a boolean and then an arbitrary number of integers and `[ (Bool+ | (Int String*)) Int? ]` is the type of lists that contain either at least one boolean, or an integer diff --git a/typing/records.md b/typing/records.md index 9f781ba..9e0b464 100644 --- a/typing/records.md +++ b/typing/records.md @@ -10,14 +10,14 @@ In Nix, there are two main uses of records - Static records: This is the classical use of records as they are used in statically typed languages: some predefined fields contain various informations about a structure. - In this setting, the labels are all statically defined as litteral - strings^[For some shameful reasons, it sometimes happens that those are - defined as a finite union of literal strings, so the rules should also support - this use-case] and the different fields are likely to contain values of - different types. + In this setting, the labels are all statically defined as expressions whose + type is type is a singleton string^[For some shameful reasons, it sometimes + happens that their type is a finite union of singleton strings, but the rules + are easy to extend to this use-case] and the different fields are likely to + contain values of different types. -- Dynamic maps: In this case, the record is used to store arbitrary key-value associations - (where the key is a string). +- Dynamic maps: In this case, the record is used to store arbitrary key-value + associations (where the key is a string). The labels here may be defined as arbitrary expressions, however most of the time the values will all be of the same type. @@ -31,10 +31,15 @@ requirements of lazy evaluation and gradual typing). We assume the existence of a distinguished constant type `$\undefr$` which represents an absent field in a record type. -We write `{ $x_1$ = $τ_1$; $\cdots$; $x_n$ = $τ_n$; }` as a shorthand for +`{ $x_1$ = $τ_1$; $\cdots$; $x_n$ = $τ_n$; _ = $τ$ }` is the type of a record +whose fields `$x_1$`, $\cdots$, `$x_n$` are respectively of type `$τ_1$`, +$\cdots$, `$τ_n$` and whose other fields are of type `$τ$` (all these fields +being possibly equal to or containing the special `$\undefr$` field meaning +that they are not defined in the record). +We write `{ $x_1$ = $τ_1$; $\cdots$; $x_n$ = $τ_n$ }` as a shorthand for `{ $x_1$ = $τ_1$; $\cdots$; $x_n$ = $τ_n$; _ = $\undefr$ }` and `{ $x_1$ = $τ_1$; $\cdots$; $x_n$ = $τ_n$; .. }` for -`{ $x_1$ = $τ_1$; $\cdots$; $x_n$ = $τ_n$; _ = Any }`. +`{ $x_1$ = $τ_1$; $\cdots$; $x_n$ = $τ_n$; _ = Any $\vee$ $\undefr$ }`. The former corresponds to a *closed* record type (i.e., a record of this type will have *exactly* the listed fields with the given types) while the latter corresponds to an *open* record type (i.e., a record of this type will have *at @@ -65,9 +70,8 @@ We have two rules for the literal records, corresponding to the two use-cases of records: - The *RFinite* rule handles the case of static records. - It applies when the labels have singleton types (or a finite union of - singleton types) and corresponds to the classical typing rule for records in - absence of dynamic labels. + It applies when the labels have singleton types and corresponds to the + classical typing rule for records in absence of dynamic labels. - The *IRInfinite* and *CRInfinite* rules handle the case of dynamic maps. In this case, we do not try to track all the elements of the record, we just @@ -114,15 +118,21 @@ There are in fact three possible cases in this formula: type $τ_x$. The type of the result may be $τ_x$ or $τ_2(x)$. This definition enjoys a natural extension to arbitrary record types (i.e., -subtypes of `{..}`), as shown by @Cas15 (a record type can be expressed as an +subtypes of `{..}`), as shown by @Cas15: a record type can be expressed as an union of atomic record types, and we extends the $+$ operator by stating that \begin{displaymath} \left(\bigvee\limits_{i \in I} τ_i\right) + \left(\bigvee\limits_{j \in J} τ_j\right) = \bigvee\limits_{i \in I,j \in J} (τ_i + τ_j) \end{displaymath} +This effectively allows us to type the union of expressions whose types are +arbitrary record types. + #### Field access +We now define the typing of expressions of the form `e1.e2` or `e1.e2 or e3` +(i.e., the access of a field of a record). + \newcommand{\defr}{\operatorname{def}} For a record type $τ = \{ x_1 = τ_1; \cdots; x_n = τ_n; \_ = τ_0 \}$, we refer to $τ_0$ by $\defr(τ)$. diff --git a/typing/types.md b/typing/types.md index 2f7efa8..cd58749 100644 --- a/typing/types.md +++ b/typing/types.md @@ -1,6 +1,6 @@ ### Presentation of the types -The types are inspired by the set-theoretic types used in the CDuce language +The types are inspired by the set-theoretic types used in the \cduce{} language and described by @Fri04. Their syntax is given alongside Nix-light's grammar in \Cref{nix-light::grammar}. @@ -38,12 +38,12 @@ problems on a lazy semantic. The reason for this is that the interpretation supposes fully evaluated values, while a lazy language manipulates possibly non-evaluated expressions, whose evaluation may never finish if forced. In particular, the `Empty` types behaves -differently: there exists no value of this type (so its interpretation as set +differently: there exists no value of this type (so its interpretation as a set is naturally the empty set), but there may be expressions of this type, which themselves may appear inside values in a lazy setting. -For example, the type `{ x = Empty }` would be not inhabited in a strict semantic -(so it would itself be a subtype of every other type, the same way as `Empty` -itself), whereas in a lazy semantic such as the one of Nix-light, it is +For example, the type `{ x = Empty }` would not be inhabited in a strict +semantic (so it would itself be a subtype of every other type, the same way as +`Empty` itself), whereas in a lazy semantic such as the one of Nix-light, it is inhabited for example by `{ x = let y = y in y; }`. It is possible to modify this interpretation to take this difference into @@ -58,3 +58,5 @@ interpretation of @Fri04. Here, it becomes $\left(\llbracket A \rrbracket \cup This new interpretation (which is described by @CP17) entails a new subtyping algorithm that fits the requirements of a lazy semantic. +It is this relation (that we note $\subtype$) that we use and extend to the +gradual subtyping relation $\subtypeG$.