03-typing.md

Typing

Judgment Forms

 1) Γ ⊢ M  :: T
 2) Γ ⊢ M  :+ Ts
 3) Γ ⊢ Ms :* Ts
 4) Γ ⊢ Ms :< T

Rules

                 Γ ⊢ M :+ T
 (t-one)       ---------------
                 Γ ⊢ M :: T


                { Γ ⊢ Msᵢ :: Tsᵢ } ^ (i ← [1 .. n])
 (t-many)      ----------------------------------------
                  Γ ⊢ Msⁿ :* Tsⁿ


                { Γ ⊢ Msᵢ :: T   } ^ (i ← [1 .. n])
 (t-gets)      ----------------------------------------
                  Γ ⊢ Msⁿ :< T


                 c has type T
 (t-con)        -----------------
                 Γ ⊢ mcon c :+ T


                 p has type T
 (t-prm)        ------------------
                 Γ ⊢ mprm p :+ T


 (t-sym)        ----------------------
                 Γ ⊢ msym S :+ tsym


                     x:T ∈ Γ
 (t-var)        ------------------
                 Γ ⊢ mvar x :+ T


                           Γ, As₁:Ts₁ ⊢ M₂ :: T₂
 (t-abt)        --------------------------------------------------
                    Γ ⊢ mabs (mpst As₁ Ts₁) M₂ :+ tall As₁ Ts₁ T₂


                           Γ, Xs₁:Ts₁ ⊢ M₂ :+ Ts₂
 (t-abm)        ------------------------------------------------
                    Γ ⊢ mabs (mpsm Xs₁ Ts₁) M₂ :+ tfun Ts₁ Ts₂


                  Γ ⊢ M₁ :: tall As₁ Ks₁ T₁    Γ ⊢ Ts₂ :* Ks₁
 (t-apt)        --------------------------------------------------
                    Γ ⊢ mapp M₁ (mgst Ts₂) :+ T₁ [ As₁ := Ts₂ ]


                  Γ ⊢ M₁ :: tfun Ts₁ Ts₂       Γ ⊢ Ms₂ :* Ts₁
 (t-apm)        -------------------------------------------------
                          Γ ⊢ mapp M₁ (mgsm Ms₂) :+ Ts₂


                  Γ ⊢ M₁ :: tfun Ts₁ Ts₂       Γ ⊢ M₂  :+ Ts₁
 (t-apv)        ------------------------------------------------
                          Γ ⊢ mapp M₁ (mgsv M₂) :+ Ts₂


                  Γ ⊢ M₁ :+ Ts₁     Γ, Xs₁:Ts₁ ⊢ M₂ :+ Ts₂
 (t-let)        ---------------------------------------------
                          Γ ⊢ mlet Xs₁ M₁ M₂ :+ Ts₂


                        { Γ ⊢ Msᵢ :* Tsᵢ } ^ i ← [1 .. n]
 (t-rec)        ----------------------------------------------
                   Γ ⊢ mrec Ls Msⁿ :+ trec Ls Tsⁿ


                   Γ ⊢ M₁ :: trec Ls Ts    l:T₁ ∈ [ (l,T) | l ← Ls | T ← Ts ]
 (t-prj)        ---------------------------------------------------------------
                          Γ ⊢ mprj M₁ l₁ :+ T₁


                                           T₂ ≡ tvnt Ls Ts
                   Γ ⊢ M₁ :: T₁            l:T₁ ∈ [ (l,T) | l ← Ls | T ← Ts ]
 (t-vnt)        ---------------------------------------------------------------
                   Γ ⊢ mvnt l₁ M₁ as T₂ :+ tvnt Ls Ts


                   Γ ⊢ M₁ :: tvnt Ls₂ Ts₂   { Γ | Ls₂:Ts₂ ⊢ Lᵢ → Mᵢ :: Tᵢ → T }
 (t-cse)        -------------------------------------------------------------------
                               Γ ⊢ mcse M₁ Ls₁ Msⁿ :+ T


                      Γ ⊢ Ms :< T
 (t-lst)       ----------------------------
                 Γ ⊢ mlst T Ms :+ tlst T


                      Γ ⊢ Ms :< T
 (t-set)       ----------------------------
                 Γ ⊢ mset T Ms :+ tset T


                    Γ ⊢ Ms₁ :< T₁    Γ ⊢ Ms₂ :< T₂
 (t-map)       -----------------------------------------
                 Γ ⊢ mmap T₁ T₂ Ms₁ Ms₂ :+ tmap T₁ T₂


                   Γ ⊢ Ms :* Ts
 (t-mmm)       ----------------------
                 Γ ⊢ mmmm Ms :+ Ts