11

I am just beginning to learn Haskell, after coming from the JavaScript/Ruby worlds. I have come across https://github.com/HoTT and the Homotopy Type Theory book, which I am very eager to read.

However, I will be learning the math and type theory concepts as I go, so it seems like it will take a long time before I understand what homotopy type theory will mean to a practicing programmer.

Could you describe what impact homotopy type theory will have on programming in practice, for a layman? For example, will it make certain things easier to easier to write? If so, which things? Or will it allow for you to do new things in programming that weren't previously possible? If so, which things?

Thanks, very much looking forward to wrapping my head around it at a more basic level.

7
  • I expect that it is, and always will remain inscrutable to practicing programmers. At best, we might get faster compilers or magical black boxes that take advantage of the mathematical-fu.
    – Telastyn
    Nov 10, 2014 at 22:58
  • Haha this is what I've been thinking so far too. I am still wondering though, is this the answer or is there something beyond what you've said? For example, could databases benefit from this? Or anything like that.
    – Lance
    Nov 11, 2014 at 0:34
  • 1
    I have no idea. I read the abstract and promptly dropped it into the bucket for inscrutable academic mumbo-jumbo.
    – Telastyn
    Nov 11, 2014 at 1:11
  • recommended reading: How do I explain ${something} to ${someone}?
    – gnat
    Nov 11, 2014 at 6:27
  • 4
    @Telastyn: If you download a book in Portuguese it will also be inscrutable as long as you haven't tried to learn the language. Why publicly denounce Portuguese books by the derogatory term mumbo-jumbo? Gödels motivation for introducing primitive recursive functions was extremely academic, in particular because the world didn't even run any programs in the 30's. I don't think just because one is a practicing programmer, academic topics will "always remain inscrutable" to your capabilities.
    – Nikolaj-K
    Apr 17, 2015 at 13:56

2 Answers 2

18

One of the powerful things compilers are able to do during their optimization phase is to swap out inefficient representations for equivalent ones. For example, in Haskell you could use a lazy list to compute a sum of numbers, but the GHC Haskell compiler will recognize that this is equivalent to using iteration with a temporary variable. That way, you get to program against a simple abstraction that's easy to reason about, while your executable takes advantage of a representation better suited to the hardware platform (and that happens to be much harder to reason about at scale).

However, equivalences known to the compiler are mostly restricted to well known and researched data structures, such as stream fusion for lists. You could define your own equivalences in source code (using a pair of conversion functions that compose to identity in either direction), but you'd have to apply them manually, and it can get tricky to choose the right type to use in all places in order to avoid excessive conversions.

Now let's imagine a world where you get to define "higher inductive types", say a canonical lookup map. This type has several constructors for the various kinds of maps: binary search, AVL, red-black, Trie, Patricia, etc. Along with the typical data constructors, you also define an equivalence type capturing possibly multiple conversions between these representations, where different conversions offer varying dimensions of efficiency (i.e., time vs. memory).

What if the compiler were able to use this notion to transparently rewrite map representations, the same way it can do today with list fusion? Meanwhile, in your code you get to work with the construction that is simplest to reason about (and makes proof work easier, if you are in such an environment). This may sound just like an abstract interfaces with multiple implementations, but it includes the freedom to choose any implementation and have the compiler transparently substitute another as needed, without affecting the meaning of the program.

HoTT gives us a type theoretic foundation to justify this fancy rewriting mechanism and these richly defined types, because it promotes the notion of equivalence to being equivalent to equality. It remains to be seen how this will actually play out in practice, but it gives us the theoretical framework on which to base future work.

2

I am new to the mathematics of type theory, but I have grasped enough to share some likely valid observation about what the univalence axiom, in particular, has to offer to software development. It is not going to be the groundbreaking (in a sense) because you are probably familiar with most of the stuff hott describes. It has connections to subtyping or interfaces (which are in fact predicates over records) being the most obvious. Yet some things are novel and I'll tell about two praised by me the most.

  1. Highly polymorphic code with extensibility

The typical codebase development starts with defining concrete types - those which carry implementation -, and abstract types - those which specify interaction. The notion of both objects (think of a java' class) and interface depicts the notion of the type in categorical sense ie something that has elements and related properties. This facility gives you the ability to create types, for example class UnorderedSet {...}, and the view of it, aka its interface; something like interface AnySet {...}, and also it would allow you to create a function that operates on any set, for example <T: Equatable, B: AnySet> bool contains(T element, B bag). This function treats any type that implements interface AnySet as equal, like ?: AnySet == ?: AnySet, meaning that you can plug into it any type that can act like a set, which in a sense of univalence axiom can be interpreted as 'OrderedSet and UnorderedSet are equal (or, better to say, equivalent)'.

There is a limitation in c-derived languages of '90s in their inability for retroactive modelling (you can't replace code without breaking any that is already existing). This problem can be framed as proving 'equalities' between types. For example, if someone would create a library for operating on geometric planes, and you have had a library for representing images (say, as a matrix), than by establishing equality between images and matrices, you would receive affine transformations and geometric warping for free. This problem is somewhat salved in newer languages like rust and swift. Not without restrictions, they both have a construct to express this intent. Here is a distilled example in rust:

use SomeGeometryLib
impl <AnyImage: Image> RepresentableAsMatrix for AnyImage { ... }

From now on you can warp and rotate it, and use it in all other relevant applications that also rely on or compatible with SomeGeometryLib. This simply means HOTT can give us better composability. Though this feature does work, the overall type system of rust and swift (two languages I know of with this feature) is rather too restrictive and I can see many more ways how it can be more expressive, leading to even more amount of reuse. PS: As far as I know, the bit about equality is not expressible even in Haskel, because I assume that it is not possible to state the relation of equivalence at the level of type classes. I may be wrong, and you should probably investigate this yourself if you want.

Another point to make is extensibility which is the part that I think relates to the fact that types do not stay in static and evolve with code bases, thus leading to a 'tomorrow our types may not be equal to themself yesterday' equality or equivalence over time. Swift and rust, have the feature of type extension, though there it is restricted to only adding new methods, which feels like artificial limitation caused by particular design choices. But in the ideal world, you'd be able to write a code that employs addition of new generic types and members after it was created, and stay backwards-compatible. Let me demonstrate with pseudocode:

//lets make a simple model of a person 
object Person { var name: String }

//then assume that you'd need to incorporate there 
//info about the place of work for example.
//you could write a special type, or use a generic parameter
object Person [PlaceOfWork] {
  var name: String
  var placeOfWork: PlaceOfWork
}
object Person {
  object PlaceOfWork {}
  var name: String
  var placeOfWork: PlaceOfWork
}
//Neither of these two approaches provides good reuse: the first one does not put enough constraints on the type variable (some may come after the type was created) and require you to carry generic context around the code (which is less troublesome in java, since it provides type erasing operation in form of a wildcard `?`; neither rust, nor swift have an equivalent), and the second one is simply limited in extensibility.

The more appropriate way would be to treat the generic context as implicitly erased, and provide a way to specify what information you'd need.

object Person {
  type PlaceOfWork
  type AlmaMatter
  var name: String
  var placeOfWork: PlaceOfWork
  var placeOfEducation: AlmaMatter
}
fn takeCollageEducatedPerson <C: CollageFacility> 
(person: Person where AlmaMatter == C) 
//can work on any person who was educated in a higher school

extension Person { type PublicOpinion; var po: PublicOpinion }
//addition of a new field does not invalidate the old code. Neat

In java, a feature like this would have been incompatible with the explicit generic signature. So to sum up this bit I can say that there may come a future where codebases are much more composable and extensible, than everything we have today.

There is also some report I have seen someday at sigplan conference if I recall correctly. It was touching matters of philosophy, and one particular statement I remember is 'A woodpecker perceive a tree in a different way than a lumberjack. What is the best way to model this?' Turns out it has a connection to hott and its equivalence :O

  1. More properties about programs ensured at the type level

There is a thing called dependent typing, which is can be described as putting more restriction on existing types. For example:

object Person { var age: Int }

This obviously is prone to errors, since the average year is a range from 1 to ~150 years, but this intent is not expressed in types, so the compiler cannot catch violations. What can you do about it? You could put checks in your code which ensure that only valid values get in, but it would work only on your side of the development and any third party could forget about these restrictions or worse - exploit them. Which is bearable for some little cases of small utilities, but unacceptable if you are writing something like banking business logic where these properties must be more than a matter of convention. You could also create a special type that handles exactly the cases of people's ages, but you wouldn't be able to substitute int with your type in any existing codebase due to the limitation of '90s languages, believe me. The way to make it work using a solution constructed from existing parts is to take an integer type and put a constraint on it - this essentially would be what is called a dependent type.

object Person { var age: Int that 'Appropriate for age description' }

In this setting, the Int type is a subtype of Int that 'Appropriate for age description'. Meaning the code is somewhat compatible with other code that works on Ints, but attempt to put here say 1000000, would be caught by a compiler as an error. Again, this is about more reuse and composability and also correctness.

Deptypes also enables you to state more intricate thing, which can be described as a predicate.

fn 'concatanete collections'
(a: Collection, b: Collection) -> result: Collection where {
  a.count + b.count == result.count
} { ... } 
//the result must have the same amount of elements as the two arguments it takes

Also, it could, in theory, express properties about things called reactive streams. Namely, you might be able to prove that certain streams perform, say, a call to a database and do not violate restrictions about system privacy, for example, while doing it.

More properties are proven - more still nights had. And also compiler can synthesise better code, due to more reasoning about properties of the code. Ideally, of course.

Simply put, HOTT gives people hints about simpler implementation for checking this stuff. Yet it is not complete and there is still development going on, which is slowed down after the sudden death of the theory initiator - Vladimir Voevodsky. Cubical Type Theory is the most recent research on the topic, but I believe that there is a long time until the theory is fully realised, and much more until it will be incorporated in the mainstream languages. Although, what hott promises is magnificent and everyone would benefit significantly from its adoption. The future can be so much better and I hope we will be around to see it blooming.

Not the answer you're looking for? Browse other questions tagged or ask your own question.