commit 58dcc27dfcc95e768acbcf7ed84ed4ce9e7b5994
parent bc9e7d18a4eb2018463764af6db809ed72c6a502
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 16 Aug 2017 17:31:03 +0200
Text for the ctor+record+variant+row types.
Diffstat:
2 files changed, 45 insertions(+), 9 deletions(-)
diff --git a/scribblings/abbreviations.rkt b/scribblings/abbreviations.rkt
@@ -1,7 +1,7 @@
#lang at-exp racket
-(provide typedracket Typedracket csharp CAML CLOS NIT CPP DeBruijn HOAS PHOAS
- monocecil dotnet DLL nanopass nanopass-c-f haskell haskell98 Hackett
- turnstile Turnstile cur Cur LaTeX C-language java lisp)
+(provide typedracket Typedracket csharp CAML OCAML CLOS NIT CPP DeBruijn HOAS
+ PHOAS monocecil dotnet DLL nanopass nanopass-c-f haskell haskell98
+ Hackett turnstile Turnstile cur Cur LaTeX C-language java lisp)
(require scribble/base
scribble/core
@@ -26,6 +26,7 @@
(define nanopass "Nanopass")
(define nanopass-c-f "Nanopass Compiler Framework")
(define CAML "CAML")
+(define OCAML "CAML")
(define CLOS "CLOS")
(define NIT "NIT")
(define CPP "C++")
@@ -36,7 +37,7 @@
(define monocecil @tt{"Mono.Cecil"})
(define dotnet ".NET")
(define DLL "DLL")
-(define haskell "haskell")
+(define haskell "Haskell")
(define haskell98 "Haskell 98")
(define Hackett "Hackett")
(define turnstile "Turnstile")
diff --git a/scribblings/adt-row-tausigma.scrbl b/scribblings/adt-row-tausigma.scrbl
@@ -8,12 +8,28 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Types (with ρ)}
+We introduce two new sorts of types: constructors and records. Constructors
+are similar to a @typedracket pair whose left element is a symbol, used as a
+tag. A constructor's tag does not need to be declared beforehand, and can be
+used on-the-fly. This makes these constructors very similar to the
+constructors used in @OCAML's polymorphic
+variants@~cite[#:precision "chapter 6" "minskyRealWorldOCaml"]. Records are
+similar to the @racket[struct]s available in @typedracket, but the accessor
+for a field is not prefixed by the name of the struct introducing that field.
+This means that the same accessor can be used to access the field in all
+records which contain that field, whereas a different accessor would be needed
+for each struct type in @|typedracket|. We also introduce row-polymorphic
+abstractions, which allow a single row type variable to range over several
+constructors or fields.
+
@cases["σ,τ" #:first-sep "⩴"
@acase{…}
@acase{@ctor[@κof[τ]]@tag*{constructor}} @; same
@acase{@record[@ςf]@tag*{possibly row-polymorphic record}} @; changed
- @acase{@∀c[(@repeated{@ρc}) τ]@tag*{row-polymorphic abstraction (constructors)}} @; new
- @acase{@∀f[(@repeated{@ρf}) τ]@tag*{row-polymorphic abstraction (fields)}}] @; new
+ @acase{@∀c[(@repeated{@ρc}) τ]
+ @tag*{row-polymorphic abstraction (constructors)}} @; new
+ @acase{@∀f[(@repeated{@ρf}) τ]
+ @tag*{row-polymorphic abstraction (fields)}}] @; new
@; new↓
@@ -28,12 +44,31 @@ constructors in the row type can be specified on variants.
@cases["σ,τ" #:first-sep "⩴"
@acase{…}
- @acase{@variant[@ςf]@tag*{possibly row-polymorphic variant}}] @; new/changed
+ @acase{@variant[@ςf]
+ @tag*{possibly row-polymorphic variant}}] @; new/changed
+
+A variant acts as the union of multiple constructor types. The variant type
+can also contain a row type variable ranging over constructors. A variant
+containing a row type variable will normally contain all the constructors used
+to instantiate that row. The constructors which are explicitly marked as
+omitted using the syntax @${-@|κ|} are however removed from the row if present
+within, and the constructors explicitly marked as present using the syntax @${
+ +@κof[τ]} will always be members of the variant. If such a constructor was
+present in the row with a different type, it is replaced by a constructor
+wrapping a value of the explicitly specified type.
@cases[@ςc #:first-sep "⩴"
@acase{@repeatset{@κof[τ]}@tag*{fixed constructors}}
- @acase{@|ρc|\ @repeatset{-@|κ|ᵢ}\ @repeatset{+@κof[ⱼ τⱼ]} @tag*{row without some ctors, with extra ctors}}]
+ @acase{@|ρc|\ @repeatset{-@|κ|ᵢ}\ @repeatset{+@κof[ⱼ τⱼ]}
+ @tag*{row without some ctors, with extra ctors}}]
+
+Similarly, records can contain a set of fields. It is also possible to use a
+row type variable ranging over constructors. The syntax @${-@|ɐ|} indicates a
+field which could be present in the row and but will not be present in the
+record type, and the syntax @${+@|ɐ|:τ} indicates a field which will always be
+present, as well as its type.
@cases[@ςf #:first-sep "⩴"
@acase{@repeatset{@|ɐ|:τ}@tag*{fixed fields}}
- @acase{@|ρf|\ @repeatset{-@|ɐ|ᵢ}\ @repeatset{+@|ɐ|ⱼ:τⱼ}@tag*{row without some fields, with extra fields}}]
+ @acase{@|ρf|\ @repeatset{-@|ɐ|ᵢ}\ @repeatset{+@|ɐ|ⱼ:τⱼ}
+ @tag*{row without some fields, with extra fields}}]
