flâneur

All Lectures

cl-l313.jonmsterling.com · saved by 1 readers

We aim to get familiar with the basic structure of dependent types. We will not treat dependent type theory as a formal system, but instead as a system of notations for a particular style of informal mathematics built up from a few basic forms of judgement. In a programming language like OCaml or Haskell, there are places in the grammar where you need to place a type, and there are other places where you need to place an element of a particular type. For example, when you write The second assertion only makes sense when the first assertion obtains. Indeed, if I had changed int -> int to a bogus piece of code that does not describe a type, then it would not be meaningful to ask whether some other code describes an “element” of this non-type! That’s because only types can have elements. Per Martin-Löf came up with some terminology that keeps all of this straight. Inspired by him, we define the following: A judgement is a specific thing that you can assert. For example “int -> int describ

We aim to get familiar with the basic structure of dependent types. We will not treat dependent type theory as a formal system, but instead as a system of notations for a particular style of informal mathematics built up from a few basic forms of judgement. In a programming language like OCaml or Haskell, there are places in the grammar where you need to place a type, and there are other places where you need to place an element of a particular type. For example, when you write The second assertion only makes sense when the first assertion obtains. Indeed, if I had changed int -> int to a bogu

related reading