www

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

adt-sub.scrbl.old (1073B)

      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)]{Subtyping}
     10 
     11 @;{
     12  @$${
     13   @$inferrule[
     14  @${\phantom{x}}
     15  @${⊢ @ctor[@κ τ] <: @ctorTop[τ]}
     16  @${@textsc{S-CtorTop}}
     17  ]
     18  }
     19 }
     20 
     21 @$${
     22  @$inferrule[
     23  @${⊢ τ <: τ'}
     24  @${⊢ @ctor[@κ τ] <: @ctor[@κ @${τ'}]}
     25  @${@textsc{S-Ctor}}
     26  ]
     27 }
     28 
     29 @$${
     30  @$inferrule[
     31  @${@repeated{⊢ τᵢ <: τ'ᵢ}}
     32  @${⊢ @record[@repeated{@${@|ɐ|ᵢ : τᵢ}}] <: @record[@repeated{@${@|ɐ|ᵢ : τ'ᵢ}}]}
     33  @${@textsc{S-Record}}
     34  ]
     35 }
     36 
     37 Permutation of the fields of a record type produces an equivalent type:
     38 
     39 @$${
     40  @$inferrule[
     41  @${\phantom{x}}
     42  @${⊢ @record[@repeated{@${@|ɐ|ᵢ : τᵢ}} @repeated{@${@|ɐ|ⱼ : τⱼ}}]
     43    <: @record[@repeated{@${@|ɐ|ⱼ : τⱼ}} @repeated{@${@|ɐ|ᵢ : τᵢ}}]}
     44  @${@textsc{S-Record-Permuation}}
     45  ]
     46 }
     47 
     48 @todo{propagate our types up/down unions like the primitive ones (I think
     49  Typed Racket does not do this everywhere it “should”).}