# Cheat sheet Common "typing judgment": Γ⊢ e:τ (Γ ::= · | Γ, x : τ) Type checking: given Γ, e and τ, find a "typing derivation". Type inference: given Γ, e, find τ and a "typing derivation". Example "typing derivation" of term "x + (x + 1)" in the F1 language: -------------- -------------- x:int⊢ x:int x:int⊢ x:int -------------- ---------------------------- x:int⊢ x:int x : int ⊢ x + 1:int ------------------------------------- x:int ⊢ x + (x + 1) : int The F1 language syntax: e ::= x | λx:τ. e | e1 e2 | n | e1 + e2 | iszero e | true | false | not e | if e1 then e2 else e3 τ ::= int | bool | τ1 → τ2 The static semantics of F1 Function rules x:τ∈ Γ Γ,x:τ0⊢ e:τ1 Γ⊢ e1:τ2→ τ1 Γ⊢ e2:τ2 -------- ---------------------- ------------------------ Γ⊢ x:τ Γ⊢ λx:τ0.e : τ0 → τ1 Γ⊢ e1 e2 : τ2 Base type rules ---------- Γ⊢ n:int Γ⊢ e1:τ2→ τ1 Γ⊢ e2:τ2 ------------------------ Γ⊢ e1 e2 : τ2 # Cheat sheet (linear) logic A ⊗ B : you’ve got A and B A & B : you can pick either A or B A ⊕ B : you get A or B (not your choice) A ⊸ B : consumes A, gives B !A : you’ve got an unlimited amount of A : linear assumption (weakening and contraction dont hold) [A] : intuitionistic assumption (weakening and contraction hold) Γ,Δ ⊢ A Γ,[A],[A] ⊢ B -------- [Id] ------- ⟨Id⟩ --------- Exchange ---------------- Contraction [A]⊢ A ⟨A⟩⊢A Δ,Γ ⊢ A Γ,[A]⊢ B Γ ⊢ B [Γ]⊢ A Γ ⊢ !A Δ,[A] ⊢ B ---------- Weakening --------- !-Intro ------------------- !-Elim Γ,[A]⊢ B [Γ]⊢ !A Γ,Δ⊢B Γ,⟨A⟩⊢ B Γ ⊢ A⊸ B Δ ⊢ A ------------ ⊸ -Intro ------------------ ⊸ -Elim Γ ⊢ A ⊸ B Γ,Δ ⊢ B Γ ⊢ A Δ ⊢ B Γ ⊢ A⊗ B Δ,⟨A⟩,⟨B⟩⊢ C --------------- ⊗ -Intro ------------------------- ⊗ -Elim Γ,Δ⊢ A⊗ B Γ,Δ ⊢ C Γ ⊢ A Γ ⊢ B Γ ⊢ A & B Γ ⊢ A & B --------------- &-Intro ----------- &-Elim-1 ----------- &-Elim-2 Γ ⊢ A & B Γ ⊢ A Γ ⊢ A Γ ⊢ A Γ ⊢ B Γ ⊢ A⊕ B Δ,⟨A⟩⊢ C Δ,⟨B⟩⊢ C ------------ ⊕ -Intro-1 ------------ ⊕ -Intro-2 ------------------------------- ⊕ -Elim Γ,Δ ⊢ A⊕ B Γ,Δ ⊢ A⊕ B Γ,Δ ⊢ C # Simple Linear Types (Phil Wadler's "Linear Types can change the world") s,t,u ::= x | λ⟨x⟩.t | s t | !t | case s of !x → u | ⟨s,t⟩ | case s of ⟨x,y⟩ → t | Inl s | Inr s | case s of Inl x → t; Inr y → u | ⟨⟨s,t⟩⟩ | Fst s | Snd s # Cheat sheet simply typed lambda calculus Typing relation between terms and types. Typing contexts or environments, which (in simply typed lambda calculus) are sets of typing assumptions. Typing assumptions take the form x:o . The typing relation Γ⊢ e:o indicates that e is a term of type o in context Γ. Instances of the typing relation are called typing judgements. t ::= t -> t | T where T in B, B = {a,b} e ::= x | \x:t.e | e e | c x:o A∈ Γ c is const. of T Γ,x:o⊢ e:t Γ,e1:o⊢ o➔ t Γ⊢ e2:o ---------- (1) ------------------ (2) -------------------- (3) ------------------------ (4) Γ⊢ x:o Γ⊢ c:T Γ⊢ (\x:o.e):(o➔ t) Γ⊢ e1 e2 : t 1. If x has type o in the context, we know that x has type o. 2. Term constants have the appropriate base types. 3. If, in a certain context with x having type o, e has type t, then, in the same context without x, \x:o.e has type o➔ t. 4. If, in a certain context, e1 has type o➔ t, and e2 has type o, then e1 e2 has type t. https://plato.stanford.edu/entries/logic-linear/ https://www.cs.colorado.edu/~bec/courses/csci5535-s09/slides/lecture18.6up.pdf https://www.cs.cmu.edu/~fp/courses/linear/handouts/linlam.pdf * proof term * proposition * natural deduction * Curry-Howard isomorphism * linear natural deduction http://www.cs.uu.nl/docs/vakken/mcpd/2019/Week%2008/Linear%20Types.pdf Γ ⊢ t : We can deduce a conclusion t from a sequence of premises Γ Γ,A,A ⊢ B Γ ⊢ B Γ,L ⊢ A ------ Identity ----------- contraction ----------- weakening --------- exchange A ⊢ A Γ,A ⊢ B Γ,A ⊢ B L,Γ ⊢ A Alternativly the sequence of premises can be treated as a set: A ∈ Γ ------- Γ ⊢ A Rules come in pairs: introduction and elimination Γ ⊢ A Γ ⊢ B -------------------- ∧ −I Γ ⊢ A ∧ B Γ ⊢ A ∧ B Γ ⊢ A ∧ B ----------- ∧ −E1 ------------- ∧ −E2 Γ ⊢ A Γ ⊢ B ⋁-introduction and elimination Γ ⊢ A Γ ⊢ B ------------- ∨ −I1 ------------- ∨ −I2 Γ ⊢ A ∨ B Γ ⊢ A ∨ B Γ ⊢ A ∨ B Γ ⊢ A ⇒ C Γ ⊢ B ⇒ C --------------------------------- ∨ −E Γ ⊢ C Implication Γ, A ⊢ B Γ ⊢ A Γ ⊢ A ⇒ B ----------- ⇒ − I ------------------- ⇒ − E Γ ⊢ A ⇒ B Γ ⊢ B Negation/False -------- ⊥ ⊢ A not (￢) is an abbreviation for A ⇒ ⊥ These rules correspond to intuitionistic or constructive interpretation of propositional logic: no rule to derive ￢￢A <=> A or (A V ￢A) Propositional logic is decidable Gentzen observed that all proofs for propositional logic can be normalised, so they only contain sub formulas of premise or conclusion: • In 1934, Curry observed a relationship between logic implication A ⇒ B and function types A ➔ B in the simply typed lambda calculus. Howard realised in 1969 that this connection is much deeper Propositional logic rules directly correspond to our typing rules: Γ,A,A ⊢ B Γ ⊢ B Γ,L ⊢ A ------ Identity ----------- contraction ----------- weakening --------- exchange A ⊢ A Γ,A ⊢ B Γ,A ⊢ B L,Γ ⊢ A which is equivalent to defining Γ to be a set and the rule A ∈ Γ ------- Γ ⊢ A which corresponds to the typing rule for variables: x : A ∈ Γ ----------- Γ ⊢ x : A • Rules for ∧ and product typing rules: TODO • Implication and the function type: TODO • ⋁-rules and the sum type: # Lecture 7: Type Checking (Programming Languages Course) # Arne Ranta (aarne@chal,ers.se) http://www.cse.chalmers.se/edu/year/2015/course/DAT150/lectures/proglang-07.html # Retrofiing Linear Types https://www.microsoft.com/en-us/research/wp-content/uploads/2017/03/linear-Jul17.pdf https://www.tweag.io/posts/2017-03-13-linear-types.html "edsko.net - Linearity, Uniqueness, and Haskell" http://edsko.net/2017/01/08/linearity-in-haskell/ "A tast of linear logic" Philip Wadler http://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf