Homotopy Type Theory and banana-rdf

Hi,

At the Scala eXchange conference I talked to Odersky ( that 'father' of Scala )
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

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.
I thought this may be of interest to you, and was interested in your feedback.

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 ( Alexander Bertails )
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.

 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

Also it is clear now that banana-rdf is based on dependent Function Types, which you can read up
in chapter 1.5 of the HoTT book.

for example for each object of RDF, such as Jena, Sesame or Plantain we have the function
that takes an instance of RDF to an specific type of RDFOps, which we could write as:

   ∏(r: RDF) RDFOps(r)

following the notation of the book.

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 15:59:31 UTC