Homotopy Type Theory ( HoTT )

Hi,

 At the Scala eXchange conference I talked to Odersky ( that 'father' of the Scala 
programming language ) about Category Theory, and he pointed me to Homotopy Type 
Theory as the mathematics that is claiming to overtake Category Theory as the foundational 
mathematical language. The book for HoTT is online, under an CC licence, and available
for LateX compilation and patches on github

 http://homotopytypetheory.org

 So as a foundational mathematical language this should be of interest to 
Philosophers. In HoTT you never have an object without a type, which if I remember
correctly was one of the key intuitions of Evans in his book The Variety of 
Reference. So in terms of a simple distinction that is à la mode one can think of

1. in set theory you start with objects, and then you group them into sets.
 It's emprical in that way
2. In category theory you also have objects but they are equivalent to the sets in set thory.
 The objects of set theory can only be reached via functions from the final object ( the object
 which has maps from all other objects ( ie. the singleton set  Because if you take the singleton
 you can create as many functions to a set as there are objects in it, and you can then name the
 objects via those functions. )
 So this is top/down or rationalist. You start with categories and maps between them, and the 
 objects of set theory fall out it.
3. HoTT you start with both. It makes sense. If you have an object
with no type, there is no way you would know what to do with it. ( is it a number, an electron, a person ? )


 From a programmatic point of view: Having read the first 60 pages, I am starting to see 
why Scala contains a very simple ( but powerful ) inferencing engine in the type system, and why
very advanced scala users tend to make types that read like proofs

 You will find that recent conference on Scala [1][2] have talks on logic programming
related issues

• lambda calculus ( the first part of the HoTT book uses typed lambda calculus )
 https://skillsmatter.com/skillscasts/5863-introduction-to-lambda-calculus
• dependent types ( the shapeless library uses that fully )
 "Scala is a language with a very sophisticated type system. It is even said to be the "poor-man's prolog"
 https://skillsmatter.com/skillscasts/5946-42-rise-of-the-dependent-types
• demysifying type inference  
 https://skillsmatter.com/skillscasts/5841-demystifying-type-inference
• Let Curry Howard Code for me
 http://scala.io/talks.html#/#NGJ-113 ( not online )
• There's a prolog in your Scala
 http://scala.io/talks.html#/#WKU-122 ( not online )

But all of what is happening there is becoming much clearer after studying HoTT.
What is interesting is that it encapsulates Category Theory, but I have
not yet reached that chapter.

 My talk "Building a Secure Distributed Social Web with Scala and Scala-JS"
also points a lot to logic - modal logic and semantic web logic and short snippets
from the history of logic/philosophy - but I have not yet worked through the connections 
with HoTT, ( the HoTT book has a section on modal logic - early ones pre David Lewis' 
Counterfactuals)

  https://skillsmatter.com/skillscasts/5960-building-a-secure-distributed-social-web-using-scala-scala-js

What is good is that I know there is a paper on Category Theory and RDF, which should help

 "Formal Modelling and Application of Graph Transformations in the Resource Description Framework"

https://www.researchgate.net/publication/40635984_Formal_Modelling_and_Application_of_Graph_Transformations_in_the_Resource_Description_Framework


Henry


[1] London Scala eXchange 2014
 https://skillsmatter.com/conferences/1948-scala-exchange-2014#program
  ( those talks can be viewed after loggin in to the skillsmatter site
   which requires an account )
[2] Paris Scala.io ( they don't have their videos online yet )
  http://scala.io/talks.html#/


Social Web Architect
http://bblfish.net/

Received on Monday, 29 December 2014 12:56:35 UTC