6 ms·

"For Dummies"? This is still not dumb enough for me. Maybe someone in the HN community can dumb it down further?

by ksikka 11y ago

jules 11y ago
How much do you know about type theory? If you know type theory then the gist of HoTT can be summarized as follows: HoTT is a dependent type theory where you have a user defined equality for each user defined type (this is what HITs, higher inductive types, are). This is a generalization of quotient types and lets you do things like integers modulo k by defining that an integer n mod k == (n+k) mod k. It also has a better equality for functions (two functions are equal if they return the same result for each input), and types (two types are equal if there is a bijection between them).
chriswarbo 11y ago
Let's say you're creating a new programming language. You think it's a good idea to use static types, but which ones? Well, everyone uses booleans, so let's include them: True : Boolean False : Boolean ("foo : bar" means "foo has type bar", or "foo is a bar"). OK, that seemed pretty easy. But wait, you've not given a type to "Boolean". For the sake of completeness: Boolean : Type Uh oh, now you need to give a type to "Type". What should it be? It turns out (via Girard's paradox) that simply saying "Type : Type" would make things inconsistent, ie. we would be able to trick the compiler into accepting incorrect programs. Instead, we use a series of "levels": Boolean : Type 0 Type n : Type (n+1) So far so good. Now let's say we want function types, for example: identity : Boolean -> Boolean identity x = x not : Boolean -> Boolean not True = False not False = True So what's this "->" thing? We can think of it as a type-level operator: it takes two types and returns a function type. In the syntax of natural deduction, we can say: a : Type n b : Type m ----------------------------- a -> b : Type (1 + max n m) ie. given "a" of type "Type n", and "b" of type "Type m", then "a -> b" has type "Type (1 + max n m)". Because the type "a -> b" somehow 'contains' the types "a" and "b", we need to ensure it's at a higher level than either of them, which is why we do "1 + max n m". In fact, there's no reason for the identity function to only work on Booleans. We can replace it with an "identity function factory", which accepts a type and returns an identity function for that type: identity : (t : Type n) -> t -> t identity x y = y Here we've re-used the "foo : bar" notation: rather than just giving the type of the first argument, we've also introduced a variable "t" representing its value (this is known as a dependent function). Notice that the definition of "identity" actually ignores the type it's been given ("x"); the implementation doesn't care what it is, it'll just return the second argument no matter what; yet we need that argument in order to type-check. When we compile this program, we can "erase" the first argument, since it has no "computational content". We can recover our original identity function, of type "Boolean -> Boolean", by applying this "identity" function to the "Boolean" type: identity Boolean : Boolean -> Boolean OK, what next? Well, since we have functions, we might as well have function composition: compose : (a : Type x) -> (b : Type y) -> (c : Type z) -> (a -> b) -> (b -> c) -> (a -> b) -> a -> c compose t1 t2 t3 g f x = f (g x) It would also be useful to have equality. Here it is for Booleans: equal : Boolean -> Boolean -> Boolean equal True x = x equal False x = not x However, just like the identity function, this isn't very satisfying. We'd like an "equality function factory", with this type: equal : (t : Type n) -> t -> t -> Boolean Except, how would we ever implement such a "factory"? It was easy for identity: we just return whatever we're given. In the case of equality, we need to inspect our arguments, to see whether they're actually equal or not. We can't do this in a way which works for all types (eg. what if we allow user-defined types?). However, there's a trick. By returning a Boolean, we're defining equality (True) and disequality (False). That's hard. Instead, we can ignore the disequality, and only focus on equality, using a different return type; let's call it "Equal x y". What does it mean for two things to be equal? It means that they're the same thing. In which case, we don't need both of them! Every value is equal to itself (a property known as "reflexivity"), so that's all we need! refl : (t : Type n) -> (x : t) -> Equal x x For example, here's equality for the Booleans: refl Boolean True : Equal True True refl Boolean False : Equal False False Note that "refl" isn't actually a function, it's a data constructor. You can think of a value like "refl Boolean True" as being a piece of data, similar to something like "pair Int String 10 'foo'"; it doesn't reduce to anything, it just gets passed around as-is. (These are often called "proof objects", but that's a bit arbitrary; a value like "pair Int String 10 'foo'" is a "proof" of "Int AND String"). If we allow computation in our types, then two different values which compute (technically: beta reduce) to the same thing are still equal by reflexivity: refl Boolean True : Equal True (not False) Here, the "not False" will compute to "True", and reflexivity will work. Different values, eg. "False" and "True", are never equal, since they don't reduce to the same thing. We can make our computations as complex as we like, for example: refl Boolean True : Equal (identity Boolean True) (compose Boolean Boolean not not True) We can even have equality between functions and equality between types: -- "identity" is equal to "identity" refl ((t : Type n) -> t -> t) identity : Equal identity identity -- "Boolean" is equal to "Boolean" refl (Type 0) Boolean : Equal Boolean Boolean We can even have equalities between equalities! -- "refl Boolean True" is equal to "refl Boolean True" refl (Equal True True) (refl Boolean True) (refl Boolean True) : Equal (refl Boolean True) (refl Boolean True) Most of this predates Homotopy Type Theory, so what are the points being made in the slides? One point is to give a topological perspective for types: a type is like a space, values in the type are like points in the space. Equalities between values are paths in the space (eg. "refl Boolean True" is a trivial path from the point "True" to itself, in the "Boolean" space). Interestingly, equalities between equalities are homotopies (smooth transformations between paths). One question we might ask is whether all equality values are the same; ie. are they all just "refl"? That's known as the "Uniqueness of Identity Proofs" (UIP), and it's an assumption that many people have been making for decades. However, if we think of equalities as paths through a space, then UIP says that all those paths can be transformed into each other. Yet that's not the case if the space contains a hole! Consider two paths going from a point X back to itself; if one of those paths loops around a hole, and the other doesn't, then there's no way to smoothly transform between the two (without "cutting and sticking"). The topological perspective also gives us some intuition about the "levels" of types: "Type 0" contains spaces with distinct points, eg. "Boolean" containing "True" and "False". These are essentially sets, from Set Theory. Although HoTT doesn't assume UIP for all types, those which do just-so-happen to "collapse" down to one value (ie. there are equalities between every point) actually occupy a level below sets; ie. they end up at "Type -1" (there's no significance to the negative number; it's just a historical accident caused by definitions like "Boolean : Type 0"). Likewise, those which add more structure occupy higher levels. One important question is how function equality behaves. It's useful to have equality for, say, Booleans, since we can compute their value and check whether they're the same. Functions are trickier: we have intensional equality (eg. Equal identity identity) but we'd like extensional equality (eg. that "identity" and "not . not" are equal, ie. Equal (identity Boolean) (compose Boolean Boolean Boolean not not)). This is tricky. If we assume extensionality as an axiom (((x : t) -> Eq (f x) (g x)) -> Eq f g), like in NuPRL, then we lose the ability to execute our programs (axioms are basically "built in primitives"; we don't know how to implement such an extensionality primitive). Observational Type Theory gets us most of the way there, but relies on UIP, which would collapse all of the higher-level structure in HoTT. Univalence is also a nice feature of HoTT. It's incompatible with UIP, but allows us to reason "up to isomorphism". For example, in set theory the sets {foo, bar} and {x, y} are isomorphic: eg. we can switch foo with x and bar with y. However, results concerning {foo, bar} may be invalid for {x, y}, since set theory lets us say things like "is foo a member of S?", which is true when S = {foo, bar} but false when S = {x, y}. HoTT doesn't let us say things like "is foo a member of type T?", hence we don't get these kind of "abstraction leaks", so our programs and proofs can be automatically lifted from one representation to another. For example, if you define a fast, distributed datastructure which is isomorphic to a linked-list, then you can automatically lift every linked-list program to your new datastructure using univalence. Unfortunately, we haven't figured out how to implement univalence yet (but many people think it's possible). Some of the results listed at the end of the slides concern the use of HoTT to prove topological results, eg. that the integers are isomorphic to paths around a hole (you can go around the hole any number of times, clockwise or anticlockwise). Girard's paradox: http://mathoverflow.net/questions/18089/what-is-the-manner-of-inconsistency-of-girards-paradox-in-martin-lof-type-theor http://mathoverflow.net/questions/18089/what-is-the-manner-o... Natural deduction: https://en.wikipedia.org/wiki/Natural_deduction https://en.wikipedia.org/wiki/Natural_deduction
- tgflynn 11y ago
  Interesting, do you think these ideas will have applications in CS ? I mean type theory is obviously useful, both to things like formal proofs and the definition of typed languages but do you think that thinking of types in terms of topological spaces and homotopy will lead to new insights in these or related areas ?
  - chriswarbo 11y ago
    It depends how you define CS; some people I work with don't consider CS and Maths to be different subjects ;) Personally, I find the topological perspective useful for thinking about types. I would guess most programmers think of types as sets, which is perfectly fine for the kind of first-order tasks we encounter in almost all day-to-day programming. However, it doesn't give much intuition when dealing with the crazy kinds of abstractions we find in languages like Coq, Agda, or even some of the funky new Haskell extensions. Whilst the vast majority of programmers will never, and should never need to, deal with that level of abstraction, it's personally the kind of programming I really enjoy :) (My own work is in the area of formal proofs, proof search, program equivalence, etc.) I think HoTT's key insight has already been made: although using UIP (or one of its many equivalents) to ignore the differences between proofs makes life easier in the short-term (eg. as a Coq user I was blown away by Agda's ability to do pretty much everything by pattern-matching on refl), in the longer term all of those transport lemmas, path inductive proofs, etc. give us tangible benefits; firstly for explaining why something is true, secondly for allowing new kinds of higher-level reasoning and thirdly for aiding mechanisation and computation. Essentially, HoTT is just a logical extension of the intuitionism/constructivism ideals :) Hopefully HoTT, or something very much like it, will narrow the gap between what people know and what machines know.
    - tgflynn 11y ago
      "Hopefully HoTT, or something very much like it, will narrow the gap between what people know and what machines know." Yeah I was actually thinking along the same lines. There seems to currently be a major disconnect in abstraction ability between humans and any AI approach I'm aware of. Humans seem to have an apparently unlimited ability to move between levels of abstraction while algorithms seem tied to the specific abstractions used in designing them. Or in other words it seems like AI algorithms are always stuck in some particular box while humans can always expand their box, or even jump to another one entirely. Unfortunately my knowledge of these fields (type theory, algebraic topology, etc.) is so limited that I have no real idea of how HoTT could help with this, beyond the vague notion that it might.
maxiepoo 11y ago
The precise technical innovations of HoTT are just that, technical. I'll try to focus on a practical consequence of those innovations. If you know anything about data structures you know that a lot of times, 2 different instances of the structure will be considered "equal" even though they aren't exactly the same. For an overly simplistic example, if you implement a list as a binary tree so that you can support things like append faster you might have a type like this: tree = node(tree, tree) | leaf(int) but you will consider things to be the same even if they aren't exactly the same tree, since you are externally presenting a list: node(node(leaf(1),leaf(2)), leaf(3)) and node(leaf(1), node(leaf(2), leaf(3)) for example. However when you implement all of your list operations (which will include tricky rebalancing), you will have to manually check it, which is hard. In HoTT you can choose to have the type system help you check it by saying tree = node(tree, tree) | leaf(int) and asserting to the type system things like node(node(t1,leaf(n)), t2) = node(t1, node(leaf(n), t2) then when you write your rebalancing function the type system will have you prove that you preserved equalities like this. You can already simulate this in theorem-proving languages but the technical details of HoTT allow you to 1) Directly encode these statements in the type system. 2) Get some properties of equality for free. 3) Lift functions on isomorphic data structures for free. The 3rd one basically means that if you prove your trees are equivalent to linked lists you can use any function that uses lists for your trees and vice-versa. All in all, if you're just interested in programming HoTT is probably not important to you. But if you work on verifying things like safety-critical systems or complicated mathematics using theorem proving assistants HoTT is probably going to be a big influence on the "next generation" of proof assistants.

"For Dummies"? This is still not dumb enough for me. Maybe someone in the HN community can dumb it down further?

by ksikka 11y ago

"For Dummies"? This is still not dumb enough for me. Maybe someone in the HN community can dumb it down further?

jules 11y ago

How much do you know about type theory? If you know type theory then the gist of HoTT can be summarized as follows: HoTT is a dependent type theory where you have a user defined equality for each user defined type (this is what HITs, higher inductive types, are). This is a generalization of quotient types and lets you do things like integers modulo k by defining that an integer n mod k == (n+k) mod k. It also has a better equality for functions (two functions are equal if they return the same result for each input), and types (two types are equal if there is a bijection between them).

chriswarbo 11y ago

Let's say you're creating a new programming language. You think it's a good idea to use static types, but which ones? Well, everyone uses booleans, so let's include them: True : Boolean False : Boolean ("foo : bar" means "foo has type bar", or "foo is a bar"). OK, that seemed pretty easy. But wait, you've not given a type to "Boolean". For the sake of completeness: Boolean : Type Uh oh, now you need to give a type to "Type". What should it be? It turns out (via Girard's paradox) that simply saying "Type : Type" would make things inconsistent, ie. we would be able to trick the compiler into accepting incorrect programs. Instead, we use a series of "levels": Boolean : Type 0 Type n : Type (n+1) So far so good. Now let's say we want function types, for example: identity : Boolean -> Boolean identity x = x not : Boolean -> Boolean not True = False not False = True So what's this "->" thing? We can think of it as a type-level operator: it takes two types and returns a function type. In the syntax of natural deduction, we can say: a : Type n b : Type m ----------------------------- a -> b : Type (1 + max n m) ie. given "a" of type "Type n", and "b" of type "Type m", then "a -> b" has type "Type (1 + max n m)". Because the type "a -> b" somehow 'contains' the types "a" and "b", we need to ensure it's at a higher level than either of them, which is why we do "1 + max n m". In fact, there's no reason for the identity function to only work on Booleans. We can replace it with an "identity function factory", which accepts a type and returns an identity function for that type: identity : (t : Type n) -> t -> t identity x y = y Here we've re-used the "foo : bar" notation: rather than just giving the type of the first argument, we've also introduced a variable "t" representing its value (this is known as a dependent function). Notice that the definition of "identity" actually ignores the type it's been given ("x"); the implementation doesn't care what it is, it'll just return the second argument no matter what; yet we need that argument in order to type-check. When we compile this program, we can "erase" the first argument, since it has no "computational content". We can recover our original identity function, of type "Boolean -> Boolean", by applying this "identity" function to the "Boolean" type: identity Boolean : Boolean -> Boolean OK, what next? Well, since we have functions, we might as well have function composition: compose : (a : Type x) -> (b : Type y) -> (c : Type z) -> (a -> b) -> (b -> c) -> (a -> b) -> a -> c compose t1 t2 t3 g f x = f (g x) It would also be useful to have equality. Here it is for Booleans: equal : Boolean -> Boolean -> Boolean equal True x = x equal False x = not x However, just like the identity function, this isn't very satisfying. We'd like an "equality function factory", with this type: equal : (t : Type n) -> t -> t -> Boolean Except, how would we ever implement such a "factory"? It was easy for identity: we just return whatever we're given. In the case of equality, we need to inspect our arguments, to see whether they're actually equal or not. We can't do this in a way which works for all types (eg. what if we allow user-defined types?). However, there's a trick. By returning a Boolean, we're defining equality (True) and disequality (False). That's hard. Instead, we can ignore the disequality, and only focus on equality, using a different return type; let's call it "Equal x y". What does it mean for two things to be equal? It means that they're the same thing. In which case, we don't need both of them! Every value is equal to itself (a property known as "reflexivity"), so that's all we need! refl : (t : Type n) -> (x : t) -> Equal x x For example, here's equality for the Booleans: refl Boolean True : Equal True True refl Boolean False : Equal False False Note that "refl" isn't actually a function, it's a data constructor. You can think of a value like "refl Boolean True" as being a piece of data, similar to something like "pair Int String 10 'foo'"; it doesn't reduce to anything, it just gets passed around as-is. (These are often called "proof objects", but that's a bit arbitrary; a value like "pair Int String 10 'foo'" is a "proof" of "Int AND String"). If we allow computation in our types, then two different values which compute (technically: beta reduce) to the same thing are still equal by reflexivity: refl Boolean True : Equal True (not False) Here, the "not False" will compute to "True", and reflexivity will work. Different values, eg. "False" and "True", are never equal, since they don't reduce to the same thing. We can make our computations as complex as we like, for example: refl Boolean True : Equal (identity Boolean True) (compose Boolean Boolean not not True) We can even have equality between functions and equality between types: -- "identity" is equal to "identity" refl ((t : Type n) -> t -> t) identity : Equal identity identity -- "Boolean" is equal to "Boolean" refl (Type 0) Boolean : Equal Boolean Boolean We can even have equalities between equalities! -- "refl Boolean True" is equal to "refl Boolean True" refl (Equal True True) (refl Boolean True) (refl Boolean True) : Equal (refl Boolean True) (refl Boolean True) Most of this predates Homotopy Type Theory, so what are the points being made in the slides? One point is to give a topological perspective for types: a type is like a space, values in the type are like points in the space. Equalities between values are paths in the space (eg. "refl Boolean True" is a trivial path from the point "True" to itself, in the "Boolean" space). Interestingly, equalities between equalities are homotopies (smooth transformations between paths). One question we might ask is whether all equality values are the same; ie. are they all just "refl"? That's known as the "Uniqueness of Identity Proofs" (UIP), and it's an assumption that many people have been making for decades. However, if we think of equalities as paths through a space, then UIP says that all those paths can be transformed into each other. Yet that's not the case if the space contains a hole! Consider two paths going from a point X back to itself; if one of those paths loops around a hole, and the other doesn't, then there's no way to smoothly transform between the two (without "cutting and sticking"). The topological perspective also gives us some intuition about the "levels" of types: "Type 0" contains spaces with distinct points, eg. "Boolean" containing "True" and "False". These are essentially sets, from Set Theory. Although HoTT doesn't assume UIP for all types, those which do just-so-happen to "collapse" down to one value (ie. there are equalities between every point) actually occupy a level below sets; ie. they end up at "Type -1" (there's no significance to the negative number; it's just a historical accident caused by definitions like "Boolean : Type 0"). Likewise, those which add more structure occupy higher levels. One important question is how function equality behaves. It's useful to have equality for, say, Booleans, since we can compute their value and check whether they're the same. Functions are trickier: we have intensional equality (eg. Equal identity identity) but we'd like extensional equality (eg. that "identity" and "not . not" are equal, ie. Equal (identity Boolean) (compose Boolean Boolean Boolean not not)). This is tricky. If we assume extensionality as an axiom (((x : t) -> Eq (f x) (g x)) -> Eq f g), like in NuPRL, then we lose the ability to execute our programs (axioms are basically "built in primitives"; we don't know how to implement such an extensionality primitive). Observational Type Theory gets us most of the way there, but relies on UIP, which would collapse all of the higher-level structure in HoTT. Univalence is also a nice feature of HoTT. It's incompatible with UIP, but allows us to reason "up to isomorphism". For example, in set theory the sets {foo, bar} and {x, y} are isomorphic: eg. we can switch foo with x and bar with y. However, results concerning {foo, bar} may be invalid for {x, y}, since set theory lets us say things like "is foo a member of S?", which is true when S = {foo, bar} but false when S = {x, y}. HoTT doesn't let us say things like "is foo a member of type T?", hence we don't get these kind of "abstraction leaks", so our programs and proofs can be automatically lifted from one representation to another. For example, if you define a fast, distributed datastructure which is isomorphic to a linked-list, then you can automatically lift every linked-list program to your new datastructure using univalence. Unfortunately, we haven't figured out how to implement univalence yet (but many people think it's possible). Some of the results listed at the end of the slides concern the use of HoTT to prove topological results, eg. that the integers are isomorphic to paths around a hole (you can go around the hole any number of times, clockwise or anticlockwise). Girard's paradox: http://mathoverflow.net/questions/18089/what-is-the-manner-of-inconsistency-of-girards-paradox-in-martin-lof-type-theor http://mathoverflow.net/questions/18089/what-is-the-manner-o... Natural deduction: https://en.wikipedia.org/wiki/Natural_deduction https://en.wikipedia.org/wiki/Natural_deduction

tgflynn 11y ago
Interesting, do you think these ideas will have applications in CS ? I mean type theory is obviously useful, both to things like formal proofs and the definition of typed languages but do you think that thinking of types in terms of topological spaces and homotopy will lead to new insights in these or related areas ?
- chriswarbo 11y ago
  It depends how you define CS; some people I work with don't consider CS and Maths to be different subjects ;) Personally, I find the topological perspective useful for thinking about types. I would guess most programmers think of types as sets, which is perfectly fine for the kind of first-order tasks we encounter in almost all day-to-day programming. However, it doesn't give much intuition when dealing with the crazy kinds of abstractions we find in languages like Coq, Agda, or even some of the funky new Haskell extensions. Whilst the vast majority of programmers will never, and should never need to, deal with that level of abstraction, it's personally the kind of programming I really enjoy :) (My own work is in the area of formal proofs, proof search, program equivalence, etc.) I think HoTT's key insight has already been made: although using UIP (or one of its many equivalents) to ignore the differences between proofs makes life easier in the short-term (eg. as a Coq user I was blown away by Agda's ability to do pretty much everything by pattern-matching on refl), in the longer term all of those transport lemmas, path inductive proofs, etc. give us tangible benefits; firstly for explaining why something is true, secondly for allowing new kinds of higher-level reasoning and thirdly for aiding mechanisation and computation. Essentially, HoTT is just a logical extension of the intuitionism/constructivism ideals :) Hopefully HoTT, or something very much like it, will narrow the gap between what people know and what machines know.
  - tgflynn 11y ago
    "Hopefully HoTT, or something very much like it, will narrow the gap between what people know and what machines know." Yeah I was actually thinking along the same lines. There seems to currently be a major disconnect in abstraction ability between humans and any AI approach I'm aware of. Humans seem to have an apparently unlimited ability to move between levels of abstraction while algorithms seem tied to the specific abstractions used in designing them. Or in other words it seems like AI algorithms are always stuck in some particular box while humans can always expand their box, or even jump to another one entirely. Unfortunately my knowledge of these fields (type theory, algebraic topology, etc.) is so limited that I have no real idea of how HoTT could help with this, beyond the vague notion that it might.

maxiepoo 11y ago

The precise technical innovations of HoTT are just that, technical. I'll try to focus on a practical consequence of those innovations. If you know anything about data structures you know that a lot of times, 2 different instances of the structure will be considered "equal" even though they aren't exactly the same. For an overly simplistic example, if you implement a list as a binary tree so that you can support things like append faster you might have a type like this: tree = node(tree, tree) | leaf(int) but you will consider things to be the same even if they aren't exactly the same tree, since you are externally presenting a list: node(node(leaf(1),leaf(2)), leaf(3)) and node(leaf(1), node(leaf(2), leaf(3)) for example. However when you implement all of your list operations (which will include tricky rebalancing), you will have to manually check it, which is hard. In HoTT you can choose to have the type system help you check it by saying tree = node(tree, tree) | leaf(int) and asserting to the type system things like node(node(t1,leaf(n)), t2) = node(t1, node(leaf(n), t2) then when you write your rebalancing function the type system will have you prove that you preserved equalities like this. You can already simulate this in theorem-proving languages but the technical details of HoTT allow you to 1) Directly encode these statements in the type system. 2) Get some properties of equality for free. 3) Lift functions on isomorphic data structures for free. The 3rd one basically means that if you prove your trees are equivalent to linked lists you can use any function that uses lists for your trees and vice-versa. All in all, if you're just interested in programming HoTT is probably not important to you. But if you work on verifying things like safety-critical systems or complicated mathematics using theorem proving assistants HoTT is probably going to be a big influence on the "next generation" of proof assistants.