3 ms·

Well, the set theoretic attempt to describe functions isn't a very nice one. Type theory gives a formal definition closer to the intuitive notion: a function f

by ihm 11y ago

Well, the set theoretic attempt to describe functions isn't a very nice one. Type theory gives a formal definition closer to the intuitive notion: a function from A to B is a program of type A -> B. I.e., a rule for turning things of type A into things of type B.

jordigh 11y ago
I admit I don't know much about type theory. I assume "program" is a term of art? Also, does this allow for functions that have literally undescribable rules, such as a function arising from the application of the axiom of choice? Wanting to allow such undescribable functions is the reason for the set theoretic definition. I assume "rule" isn't a term of art? What's the book to read for this stuff?
- ihm 11y ago
  Yes, program is a term of art. It means a "term" in the type theory under consideration. A type theory is essentially a programming language with a fancy type system, and there are many type theories, just as there are many programming languages. It does allow for functions without computable rules. In the case of the axiom of choice, one postulates as an axiom a program with a type that says something like "give me a type A and an A-indexed family of types, P : A -> Type, such that for all a:A, the type P a is non-empty, and I'll give you a function f : (a : A) -> P a". As far as I know, there is still no one comprehensive book on type theory. I think the type theory parts of the homotopy type theory book (https://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf https://hottheory.files.wordpress.com/2013/03/hott-online-61...) are quite good. Chapter 1 gives the basics of dependent type theory. Chapter 2 is about the groupoid interpretation of type theory and is quite nice. Chapter 3 is about "logical things" in type theory (things like axiom of choice). Chapter 5 is about inductive types which are quite central to type theory (these are generalizations of algebraic data types like trees and lists from functional programming languages).

by ihm 11y ago

jordigh 11y ago

I admit I don't know much about type theory. I assume "program" is a term of art? Also, does this allow for functions that have literally undescribable rules, such as a function arising from the application of the axiom of choice? Wanting to allow such undescribable functions is the reason for the set theoretic definition. I assume "rule" isn't a term of art? What's the book to read for this stuff?

ihm 11y ago
Yes, program is a term of art. It means a "term" in the type theory under consideration. A type theory is essentially a programming language with a fancy type system, and there are many type theories, just as there are many programming languages. It does allow for functions without computable rules. In the case of the axiom of choice, one postulates as an axiom a program with a type that says something like "give me a type A and an A-indexed family of types, P : A -> Type, such that for all a:A, the type P a is non-empty, and I'll give you a function f : (a : A) -> P a". As far as I know, there is still no one comprehensive book on type theory. I think the type theory parts of the homotopy type theory book (https://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf https://hottheory.files.wordpress.com/2013/03/hott-online-61...) are quite good. Chapter 1 gives the basics of dependent type theory. Chapter 2 is about the groupoid interpretation of type theory and is quite nice. Chapter 3 is about "logical things" in type theory (things like axiom of choice). Chapter 5 is about inductive types which are quite central to type theory (these are generalizations of algebraic data types like trees and lists from functional programming languages).