Skip to content

Instantly share code, notes, and snippets.

@andrcmdr

andrcmdr/λcube.md

Forked from brendanzab/λcube.md
Last active February 21, 2025 12:28
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save andrcmdr/7121c3d9eb83f06785d8055a5c3604a3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save andrcmdr/7121c3d9eb83f06785d8055a5c3604a3 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. andrcmdr revised this gist Feb 12, 2020. 1 changed file with 53 additions and 22 deletions.
    75 changes: 53 additions & 22 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -1,6 +1,6 @@
    ### System λ

    The untyped lambda calculus
    The untyped Lambda Calculus

    ```
    e ::= terms:
    @@ -11,9 +11,9 @@ e ::= terms:

    ### System λ→

    The simply Typed Lambda Calculus
    The first-order simply typed Lambda Calculus (Propositional Calculus/Logic)

    - Terms depending on terms
    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)

    ```
    k :: = kinds:
    @@ -41,8 +41,10 @@ idInt = λ x : int . x

    ### System λΠ

    - Terms depending on terms
    - Types depending on terms
    The first-order dependently typed Lambda Calculus (Predicate Calculus/Logic)

    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
    - Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)

    ```
    t ::= types:
    @@ -54,14 +56,16 @@ e ::= terms:
    x variable
    e e application
    λ x : t . e abstraction
    ````
    ```

    ### System λ2

    - Terms depending on terms
    - Terms depending on types
    The second-order polymorphic typed Lambda Calculus (Propositional Calculus/Logic)

    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
    - Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)

    ```diff
    ```
    k :: = kinds:
    * type of types
    @@ -79,8 +83,10 @@ e ::= terms:

    ### System λω_

    - Terms depending on terms
    - Types depending on types
    The (weakly) higher-order (higher-kinded) typed Lambda Calculus (Propositional Calculus/Logic), Type Constructors

    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
    - Types depending on types (allows types to depend on types, i.e. types that can bind types)

    ```
    k :: = kinds:
    @@ -99,16 +105,37 @@ e ::= terms:
    λ x : t . e abstraction
    ```

    ### System λΠ2 (λP2)

    The second-order dependently typed polymorphic Lambda Calculus (Predicate Calculus/Logic)

    λΠ + λ2

    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
    - Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
    - Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)

    ### System λΠω_ (λPω_)

    The (weakly) higher-order (higher-kinded) dependently typed Lambda Calculus (Predicate Calculus/Logic)

    λΠ + λω_

    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
    - Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
    - Types depending on types (allows types to depend on types, i.e. types that can bind types)

    ### System λω

    Haskell, Standard ML, OCaml, F#, Scala 2
    The higher-order (higher-kinded) typed polymorphic Lambda Calculus (Propositional Calculus/Logic)

    λ2 + λω_
    Standard ML, OCaml, F#, Nemerle, Haskell, Scala 2

    - Terms depending on terms
    - Terms depending on types
    - Types depending on types
    λ2 + λω_

    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
    - Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)
    - Types depending on types (allows types to depend on types, i.e. types that can bind types)

    ```
    k :: = kinds:
    @@ -134,14 +161,18 @@ id : ∀ a : * . a → a
    id = Λ a : * . λ x : a . x
    ```

    ### System λΠω (Calculus of Constructions)
    ### System λΠω (λPω, λC)

    The higher-order (higher-kinded) dependently typed polymorphic Lambda Calculus (CoC - Calculus of Constructions)

    Dependent ML, ATS, F*, Coq/Gallina, Matita, ALF, Cayenne, Epigram, Lean, LEGO, Agda, Idris, Ur/Web, Scala 3 (DOTty - Dependent Object Types)

    Dependent ML, ALF, Cayenne, Epigram, LEGO, Agda, Idris, Lean, F*, Coq, Matita, Scala 3 (Dotty), Ur/Web
    λΠ + λ2 + λω_

    - Terms depending on terms
    - Terms depending on types
    - Types depending on types
    - Types depending on terms
    - Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
    - Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
    - Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)
    - Types depending on types (allows types to depend on types, i.e. types that can bind types)

    ```
    e ::=
  2. andrcmdr revised this gist Aug 15, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -101,7 +101,7 @@ e ::= terms:

    ### System λω

    Haskell, Elm, Standard ML, OCaml, F#, Scala 2
    Haskell, Standard ML, OCaml, F#, Scala 2

    λ2 + λω_

  3. andrcmdr revised this gist Jul 8, 2017. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -136,7 +136,7 @@ id = Λ a : * . λ x : a . x

    ### System λΠω (Calculus of Constructions)

    Dependent ML, ALF, Cayenne, Epigram, LEGO, Agda, Idris, Lean, Coq, F*, Matita, Scala 3 (Dotty), Ur/Web
    Dependent ML, ALF, Cayenne, Epigram, LEGO, Agda, Idris, Lean, F*, Coq, Matita, Scala 3 (Dotty), Ur/Web

    - Terms depending on terms
    - Terms depending on types
    @@ -150,4 +150,4 @@ e ::=
    e e application
    ∀ x : e . e quantification (∀ + Π)
    λ x : e . e abstraction (λ + Λ)
    ````
    ```
  4. andrcmdr revised this gist Jul 7, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -136,7 +136,7 @@ id = Λ a : * . λ x : a . x

    ### System λΠω (Calculus of Constructions)

    Idris, Agda, Lean, Coq, F*, Matita, Scala 3 (Dotty), Ur/Web
    Dependent ML, ALF, Cayenne, Epigram, LEGO, Agda, Idris, Lean, Coq, F*, Matita, Scala 3 (Dotty), Ur/Web

    - Terms depending on terms
    - Terms depending on types
  5. andrcmdr revised this gist Jul 7, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -136,7 +136,7 @@ id = Λ a : * . λ x : a . x

    ### System λΠω (Calculus of Constructions)

    Idris, Agda, Lean, Coq, F*, Scala 3 (Dotty), Ur/Web
    Idris, Agda, Lean, Coq, F*, Matita, Scala 3 (Dotty), Ur/Web

    - Terms depending on terms
    - Terms depending on types
  6. andrcmdr revised this gist Jun 30, 2017. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -101,7 +101,7 @@ e ::= terms:

    ### System λω

    Haskell, SML, Ocaml, Elm
    Haskell, Elm, Standard ML, OCaml, F#, Scala 2

    λ2 + λω_

    @@ -136,7 +136,7 @@ id = Λ a : * . λ x : a . x

    ### System λΠω (Calculus of Constructions)

    Idris, Agda, Lean, Coq, Scala 3 (Dotty), Ur/Web
    Idris, Agda, Lean, Coq, F*, Scala 3 (Dotty), Ur/Web

    - Terms depending on terms
    - Terms depending on types
  7. andrcmdr revised this gist Jun 30, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -136,7 +136,7 @@ id = Λ a : * . λ x : a . x

    ### System λΠω (Calculus of Constructions)

    Idris, Agda, Lean, Coq
    Idris, Agda, Lean, Coq, Scala 3 (Dotty), Ur/Web

    - Terms depending on terms
    - Terms depending on types
  8. @brendanzab brendanzab revised this gist Oct 25, 2016. 1 changed file with 29 additions and 7 deletions.
    36 changes: 29 additions & 7 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -11,11 +11,14 @@ e ::= terms:

    ### System λ→

    The simply Typed Lambda Calculus)
    The simply Typed Lambda Calculus

    - Terms depending on terms

    ```
    k :: = kinds:
    * type of types
    t ::= types:
    a variable
    t → t arrow type
    @@ -26,6 +29,16 @@ e ::= terms:
    λ x : t . e abstraction
    ```

    Where `bool : *` and `int : *`

    ```
    idBool : bool → bool
    idBool = λ x : bool . x
    idInt : int → int
    idInt = λ x : int . x
    ```

    ### System λΠ

    - Terms depending on terms
    @@ -43,7 +56,7 @@ e ::= terms:
    λ x : t . e abstraction
    ````
    ### System λ2 (System F)
    ### System λ2
    - Terms depending on terms
    - Terms depending on types
    @@ -64,7 +77,7 @@ e ::= terms:
    Λ a : k . e type abstraction
    ```

    ### System λω_ (System Fω_)
    ### System λω_

    - Terms depending on terms
    - Types depending on types
    @@ -86,7 +99,9 @@ e ::= terms:
    λ x : t . e abstraction
    ```

    ### System λω (System Fω)
    ### System λω

    Haskell, SML, Ocaml, Elm

    λ2 + λω_

    @@ -114,8 +129,15 @@ e ::= terms:
    Λ a : k . e type abstraction
    ```

    ```
    id : ∀ a : * . a → a
    id = Λ a : * . λ x : a . x
    ```

    ### System λΠω (Calculus of Constructions)

    Idris, Agda, Lean, Coq

    - Terms depending on terms
    - Terms depending on types
    - Types depending on types
    @@ -126,6 +148,6 @@ e ::=
    x variables
    * type of types
    e e application
    ∀ x : e . e quantification (∀ and Π)
    λ x : e . e abstraction (λ and Λ)
    ````
    ∀ x : e . e quantification (∀ + Π)
    λ x : e . e abstraction (λ + Λ)
    ````
  9. @brendanzab brendanzab revised this gist Oct 25, 2016. 1 changed file with 83 additions and 76 deletions.
    159 changes: 83 additions & 76 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -3,111 +3,118 @@
    The untyped lambda calculus

    ```
    e ::=
    x
    e e
    λ x. e
    e ::= terms:
    x variable
    e e application
    λ x . e abstraction
    ```

    ### System λ→

    The simply Typed Lambda Calculus)

    - Terms depending on terms

    ```
    t ::=
    x
    t → t
    e ::=
    x
    e e
    λ x : t . e
    t ::= types:
    a variable
    t → t arrow type
    e ::= terms:
    x variable
    e e application
    λ x : t . e abstraction
    ```

    ### System λ2
    ### System λΠ

    - Terms depending on terms
    - Terms depending on types
    - Types depending on terms

    ```
    k :: =
    *
    t ::= types:
    a variable
    t → t arrow type
    Π x : t . e abstraction
    e ::= terms:
    x variable
    e e application
    λ x : t . e abstraction
    ````
    t ::=
    x
    t → t
    ∀ a . t
    ### System λ2 (System F)
    e ::=
    x
    e e
    λ x : t . e
    Λ a : k . e
    ```
    - Terms depending on terms
    - Terms depending on types
    ```
    id : ∀ a . a → a
    id = Λ a : * . λ x : a . x
    ```diff
    k :: = kinds:
    * type of types
    t ::= types:
    a variable
    t → t arrow type
    e ::= terms:
    x variable
    e e application
    λ x : t . e abstraction
    e t type application
    Λ a : k . e type abstraction
    ```

    ### System λω_
    ### System λω_ (System Fω_)

    - Terms depending on terms
    - Types depending on types

    ```
    k :: =
    *
    k → k
    t ::=
    x
    t → t
    ∀ a : k . t
    e ::=
    x
    e e
    λ x : t . e
    Λ a : k . e
    k :: = kinds:
    * type of types
    k → k arrow kind
    t ::= types:
    a variable
    t → t arrow type
    t t application
    ∀ a : k . t universal quantification
    e ::= terms:
    x variable
    e e application
    λ x : t . e abstraction
    ```

    ### System λω
    ### System λω (System Fω)

    λ2 + λω_

    - Terms depending on terms
    - Terms depending on types
    - Types depending on types


    ```
    k ::= *
    t ::=
    a
    ∀ a : k . t
    e ::=
    x
    e e
    λ x : t . e
    Λ a : k . e
    k :: = kinds:
    * type of types
    k → k arrow kind
    t ::= types:
    a variable
    t → t arrow type
    t t application
    ∀ a : k . t universal quantification
    e ::= terms:
    x variable
    e e application
    λ x : t . e abstraction
    e t type application
    Λ a : k . e type abstraction
    ```

    ### System λΠ

    - Terms depending on terms
    - Types depending on terms

    ```
    e ::=
    x
    *
    e e
    ∀ x : e . e
    λ x : e . e
    ````
    ### System λΠω
    ### System λΠω (Calculus of Constructions)

    - Terms depending on terms
    - Terms depending on types
    @@ -116,9 +123,9 @@ e ::=

    ```
    e ::=
    x
    *
    e e
    ∀ x : e . e
    λ x : e . e
    x variables
    * type of types
    e e application
    ∀ x : e . e quantification (∀ and Π)
    λ x : e . e abstraction (λ and Λ)
    ````
  10. @brendanzab brendanzab revised this gist Oct 25, 2016. 1 changed file with 81 additions and 5 deletions.
    86 changes: 81 additions & 5 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -1,4 +1,6 @@
    System λ
    ### System λ

    The untyped lambda calculus

    ```
    e ::=
    @@ -7,20 +9,75 @@ e ::=
    λ x. e
    ```

    System λ→
    ### System λ→

    - Terms depending on terms

    ```
    t ::=
    x
    t → t
    e ::=
    x
    e e
    λ x : t . e
    ```

    ### System λ2

    - Terms depending on terms
    - Terms depending on types

    ```
    k :: =
    *
    t ::=
    x
    t → t
    ∀ a . t
    e ::=
    x
    e e
    λ x : t . e
    Λ a : k . e
    ```

    System λω
    ```
    id : ∀ a . a → a
    id = Λ a : * . λ x : a . x
    ```

    ### System λω_

    - Terms depending on terms
    - Types depending on types

    ```
    k :: =
    *
    k → k
    t ::=
    x
    t → t
    ∀ a : k . t
    e ::=
    x
    e e
    λ x : t . e
    Λ a : k . e
    ```

    ### System λω

    - Terms depending on terms
    - Terms depending on types
    - Types depending on types


    ```
    k ::= *
    @@ -36,7 +93,26 @@ e ::=
    Λ a : k . e
    ```

    System λPω
    ### System λΠ

    - Terms depending on terms
    - Types depending on terms

    ```
    e ::=
    x
    *
    e e
    ∀ x : e . e
    λ x : e . e
    ````
    ### System λΠω
    - Terms depending on terms
    - Terms depending on types
    - Types depending on types
    - Types depending on terms
    ```
    e ::=
    @@ -45,4 +121,4 @@ e ::=
    e e
    ∀ x : e . e
    λ x : e . e
    ```
    ````
  11. @brendanzab brendanzab revised this gist Oct 24, 2016. 1 changed file with 10 additions and 3 deletions.
    13 changes: 10 additions & 3 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -1,13 +1,18 @@
    System λ

    ```
    e ::= x | e e | λ x. e
    e ::=
    x
    e e
    λ x. e
    ```

    System λ→

    ```
    t ::= x | t → t
    t ::=
    x
    t → t
    e ::=
    x
    @@ -20,7 +25,9 @@ System λω
    ```
    k ::= *
    t ::= a | ∀ a : k . t
    t ::=
    a
    ∀ a : k . t
    e ::=
    x
  12. @brendanzab brendanzab revised this gist Oct 24, 2016. 1 changed file with 8 additions and 6 deletions.
    14 changes: 8 additions & 6 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -1,9 +1,13 @@
    System λ

    ```
    e ::= x | e e | λ x. e
    ```

    System λ→

    ```
    t ::=
    x
    t → t
    t ::= x | t → t
    e ::=
    x
    @@ -16,9 +20,7 @@ System λω
    ```
    k ::= *
    t ::=
    a
    ∀ a : k . t
    t ::= a | ∀ a : k . t
    e ::=
    x
  13. @brendanzab brendanzab created this gist Oct 24, 2016.
    39 changes: 39 additions & 0 deletions λcube.md
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,39 @@
    System λ→

    ```
    t ::=
    x
    t → t
    e ::=
    x
    e e
    λ x : t . e
    ```

    System λω

    ```
    k ::= *
    t ::=
    a
    ∀ a : k . t
    e ::=
    x
    e e
    λ x : t . e
    Λ a : k . e
    ```

    System λPω

    ```
    e ::=
    x
    *
    e e
    ∀ x : e . e
    λ x : e . e
    ```