www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

adt-row-shorthands.scrbl (2412B)

      1 #lang scribble/manual
      2 
      3 @require["util.rkt"
      4          "adt-utils.rkt"
      5          (for-label (only-meta-in 0 typed/racket))]
      6 @(use-mathjax)
      7 
      8 @title[#:style (with-html5 manual-doc-style)
      9        #:version (version-text)]{Shorthands (with ρ)}
     10 
     11 The polymorphic builder function for the @κ constructor which
     12 intuitively corresponds to @ctore[κ] can be written as the η-expansion of the
     13 @ctore[κ e] operator:
     14 
     15 @$${@Λe[(α) @λe[(@${x : α}) @ctore[κ x]]]}
     16 
     17 The same applies to the predicate form of constructors:
     18 
     19 @$${@λe[(@${x : ⊤}) @app[@ctor-pred[κ] x]]}
     20 
     21 The same applies to the accessor for a constructor's encapsulated value:
     22 
     23 @$${@Λe[(α) @λe[(@${x : @ctorτ[κ α]}) @app[@ctor-val[κ] x]]]}
     24 
     25 As a convenience, we will write @ctore[κ], @ctor-pred[κ] and @ctor-val[κ] as a
     26 shorthand for the above lambda functions.
     27 
     28 As per the typing rules given in @secref{adt-row-trules}, these functions have
     29 the following types:
     30 
     31 @htodo{The rules below are the same??? Probably an unfinished copy-paste}
     32 
     33 @$inferrule[-
     34             @${Γ ⊢ @ctorτ[κ] : @∀r[(α) @f→[(α) @R[@ctorτ[κ α] ϵ ⊥ ∅]]]}
     35             @${@textsc{T-Shorthand-Ctor}}]
     36 
     37 @todo{Write their types here too.}
     38 
     39 
     40 The polymorphic builder function for a record which
     41 intuitively corresponds to @recorde[@repeated{@ɐ}] can be written as the
     42 η-expansion of the @recorde[@repeated{@ɐ = e}] operator:
     43 
     44 @$${
     45  @Λe[(@repeated{αᵢ}) @λe[(@repeated{xᵢ : αᵢ}) @recorde[@repeated{@|ɐ|ᵢ = xᵢ}]]]
     46 }
     47 
     48 The same applies to the predicate forms of record types:
     49 
     50 @;{
     51  @$${
     52   @aligned{
     53    &(λ ([x : ⊤])\\
     54    &\quad(Λ (@repeated{αᵢ})\\
     55    &\qquad(λ (@repeated{[pᵢ : (⊤ \xrightarrow[∅]{αᵢ|\overline{αᵢ}} Boolean)]})\\
     56    &\qquad\quad(@record-pred[@repeatset{@|ɐ|ᵢ ? pᵢ}] x))}\\
     57  }
     58 }
     59 
     60 @$${
     61  \begin{gathered}
     62  @λe[(@${x : ⊤}) @app[@record-pred[@repeatset{@|ɐ|ᵢ}] x]] \\
     63  @λe[(@${x : ⊤}) @app[@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}] x]]
     64  \end{gathered}
     65 }
     66 
     67 The same applies to the accessor for a field of a record:
     68 
     69 @$${@Λe[(α) @Λfe[(@ρf) @λe[(@${x : @recorde[@ρf @${+@|ɐ|:τ}]})
     70                            @record-gete[x @ɐ]]]]}
     71 
     72 @todo{Write their types here too.}
     73 
     74 As a convenience, we will write @recorde[@repeated{@ɐ}],
     75 @record-pred[@repeatset{@|ɐ|ᵢ}],
     76 @record-pred[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}] and @record-gete[ɐ] as
     77 shorthands for the above lambda functions.