adt.scrbl (2715B)
1 #lang scribble/manual 2 3 @require["util.rkt" 4 (for-label (only-meta-in 0 typed/racket))] 5 @(use-mathjax) 6 7 @title[#:style (with-html5 manual-doc-style) 8 #:version (version-text) 9 #:tag "adt-chap"]{Extension of Typed Racket with algebraic 10 datatypes and row polymorphism} 11 12 We extend the formalisation 13 from@~cite[#:precision "pp. 62, 72 and 92" "tobin-hochstadt_typed_2010"]. 14 15 @require["adt-utils.rkt"] 16 17 @asection{ 18 @atitle{Notations} 19 20 We use the same notations as in 21 @secref["from-dissertation-tobin-hochstadt" 22 #:doc '(lib "phc-thesis/scribblings/phc-thesis.scrbl")]. Additionally, 23 we use @ρc to denote a row type variable abstracting over a set of 24 constructors, and we use @ρf to denote a row type variable abstracting over a 25 set of fields. The occurrences of @${c} and @${f} in this context are purely 26 syntactical, and only serve the purpose of distinguishing between the two 27 notations — the one for constructors, and the one for fields. 28 29 We define the universe of constructor names @${𝒞} as being equivalent to the 30 set of strings of unicode characters@htodo{Check in the implementation that 31 this is not equivalent to the set of symbols, as these cannot be serialised.}, 32 and the universe of field names @${ℱ} likewise (the distinction resides only 33 in their intended use). Constructor and field names are compile-time 34 constants, i.e. they are written literally in the program source. 35 36 @$${@κ ⩴ name ∈ 𝒞} 37 @$${@ɐ ⩴ name ∈ ℱ} 38 } 39 40 @include-asection["adt-row-tausigma.scrbl"] 41 @include-asection["adt-row-e.scrbl"] 42 @include-asection["adt-row-v.scrbl"] 43 @include-asection["adt-row-Ectx.scrbl"] 44 @include-asection["adt-row-te.scrbl"] 45 @include-asection["adt-row-sub.scrbl"] 46 @include-asection["adt-row-pe.scrbl"] 47 @include-asection["adt-row-trules.scrbl"] 48 @include-asection["adt-row-opsem.scrbl"] 49 @include-asection["adt-row-shorthands.scrbl"] 50 51 @;{ 52 Primitive operations: 53 54 @$${c ⩴ … @P @textit{ctor-val}} 55 } 56 57 @todo{Argue that, setting aside concerns like serialisation and performance, a 58 type system with symbols, unique tokens (a way to create a fresh "identity", 59 like (cons 0 0) creates a fresh memory cell which is not eq? to any other, 60 past or future), untagged unions, pure case→ functions with the usual 61 polymorphism and row polymorphism (ranging over function cases, with 62 negation), i.e. a simplification / generalisation of our system, is more 63 "general" than @typedracket (i.e. Racket's existing types can be easily 64 encoded with ours), and show how other systems of variants and records can be 65 encoded with it (try the one from @CAML + the "backtick" cases of variants; 66 try to see if the one from tinybang is more general, less or different).}