# Type Theory

- Page: https://shared.btbytes.com/p/type-theory
- Date: 2018-03-06

## Introductory materials

- [Learn Type Theory](http://web.archive.org/web/20150823072824/http://jozefg.bitbucket.org/posts/2015-08-14-learn-tt.html)
- [Type Theory in 15 minutes](https://github.com/nikivazou/presentations/blob/master/type-theory-in-15-min/type-theory-in-15min.pdf) [presentation in PDF].


Important concepts in type theory.

-   Alonzo Church's typed lambda-calculus -- mathematical foundation
-   Per Martin-Löf's intuitionistic type theory, 1998
    :cite:martin1998intuitionistic

-   Curry-Howard correspondence -- equates programs with proofs.

- [Homotopy type theory](http://homotopytypetheory.org/) refers to a new
interpretation of Martin-Löf’s system of intensional, constructive type
theory into abstract homotopy theory.


## Type inference

[Type Inference by Solving Constraints – Caleb Helbling – Programming Languages & Systems](http://web.archive.org/web/20180304210113/http://www.calebh.io/Type-Inference-by-Solving-Constraints/)

## Videos

- "Type Theory Foundations" lecture by Robert Harper at [OPLSS
    2013](http://www.cs.uoregon.edu/research/summerschool/summer13/curriculum.html).

## To read

-   "Programming in Martin-Lof's type theory" by Nordstrom, 1990    cite:[Nordstrom1990]


## Row polymorphism vs subtyping


- [Row Polymorphism Isn't Subtyping - BAM Weblog](https://brianmckenna.org/blog/row_polymorphism_isnt_subtyping)
- [typing - What are the major differences between row polymorphism and subtyping - Computer Science Stack Exchange](http://cs.stackexchange.com/questions/53998/what-are-the-major-differences-between-row-polymorphism-and-subtyping)

- [Objects and Aspects: Row Polymorphism](https://www.cs.cmu.edu/~neelk/rows.pdf) -- Neel Krishnaswami


## Misc

- [types.markdown](https://gist.github.com/garybernhardt/122909856b570c5c457a6cd674795a9c?) and [discussion](https://news.ycombinator.com/item?id=12349384)