Re: Category Theory CG? was: Algebraic Property Graphs and RDF

> On 14 Nov 2019, at 11:46, Hugh Glaser <hugh@glasers.org> wrote:
> 
> I love the ideas of Category Theory.
> I even used them to inform the way I did my course in Maths for first year CS.
> 
> However... :-)
> When I used to be Functional, there was a lot of ferment on CT around Functional Programming, Abstract Interpretation, Strictness Analysis, etc., which consumed quite a lot of energy.
> (I spent pleasant hours listening to some stunning seminars from Samson and others!)
> It was clearly good for modelling and thinking about things (as with my course), but it is not clear to me that it ever actually advanced stuff by *using* it.
> And my maths friends seemed to suggest that what was being done wasn't much more than the simplest (to them) stuff.
> 
> So now I wonder whether we are in the same world - all very seductive and interesting, but will it get anywhere useful?

Clearing conceptual confusion is a preliminary to being able to do certain things,
so if it only just did that it would be very useful. Thinking of the earth as round,
allowed one to forge the project of sailing around it for example.

From a practical point of view, I noticed that Odersky and Philip Wadler was the one behind Java Generics. See this paper.
http://www-edlab.cs.umass.edu/cs530/gj-oopsla.pdf
Wadler of course is well known in functional programming.
The work on Java Generics lead to Scala over time.
Scala is what is behind Twitter. So at least one can say it has impact.

And as I mentioned yesterday, Odersky is the one who pointed me to HoTT,
which gives a whole new view on the Curry Howard isomorphism, and on the
the deep relation between programs, topology  and logic. 

The work on Linear Types which Abramsky gave a formalization in terms of 
categories of Games is what lead to Rust. Rust is currently one of the most
popular languages out there.

In any case conferences in the Scala world (which I know of best) 
have keynotes introducing Category Theory.  I recommend Bartosz Milewski’s 
Category Theory for Programmers
https://github.com/hmemcpy/milewski-ctfp-pdf

Something changed in the past 30 years. In the late 1980ies CT was
still abstract nonsense. Now programmers go to conferences to learn it.
Universities should catch on to this.

> 
> So having a group that goes off and tries to leverage CT to make some advances seems a great idea to me.
> And I look forward to it reporting back on those advances!
> 
> Best
> Hugh
> 
>> On 14 Nov 2019, at 09:39, Henry Story <henry.story@bblfish.net> wrote:
>> 
>> 
>> 
>>> On 14 Nov 2019, at 00:03, Ryan Wisnesky <ryan@conexus.com> wrote:
>>> 
>>> I think a key function of the list will be educational.  For example, in reading your message, I find myself wanting to deliver a lecture on how domain theory and category theory relate, similar to lectures I myself learned from in grad school.
>> 
>> I look forward to that. I need to learn at least a bit of Domain Theory as it
>> comes up in work by Abramsky who is known for his analysis of programming 
>> languages using  categories of games.
>> 
>> ( An short introduction: ”From CSP to Game Semantics"
>> https://www.researchgate.net/profile/Samson_Abramsky/publication/225855136_From_CSP_to_Game_Semantics/links/0deec52da933530e12000000.pdf )
>> 
>> Interestingly in recent work he looks at how this ties to HoTT and also access control.
>> 
>>> 
>>>> On Nov 13, 2019, at 1:31 PM, Martynas Jusevičius <martynas@atomgraph.com> wrote:
>>>> 
>>>> 
>>>> Hi Henry,
>>>> 
>>>> I’m curious about practical implications on software development.
>>>> 
>>>> I don’t know anything about CT, but the dependent types and functions in your blog post read a lot like domains and functions in denotational semantics:
>>>> http://people.cs.ksu.edu/~schmidt/text/DenSem-full-book.pdf#page=27
>>>> 
>>>> I have used DS to (attempt to) formalize Linked Data Templates - SPARQL-based definitions of Linked Data APIs:
>>>> https://atomgraph.github.io/Linked-Data-Templates/
>>>> 
>>>> Your examples seem to model HTTP interactions. But I think it’s the server processing of interactions that needs to be modeled, if we are aiming for formal interoperability on the web
>> 
>> There are a lot of things that can be modeled :-)
>> 
>> I think the HTTP side of things should be analyzed coalgebraically, which
>> is the dual of algebras, and the mathematics of infinite streams, processes, 
>> systems, OO programming, and in which modal logic plays a key role.
>> 
>> Weirdly enough if one looks at it, the W3C works mostly on the algebraic side,
>> whereas the IETF on the coalgebraic side.
>> 
>> Anyway, that just gives an idea of the many fun things one can discuss in 
>> such a group.
>> 
>> Henry
>> 
>>>> 
>>>> Martynas
>>>> atomgraph.com
>>>> 
>>>> On Wed, 13 Nov 2019 at 11.18, Henry Story <henry.story@bblfish.net> wrote:
>>>> Hi all,
>>>> 
>>>>   we have been discussing the possibility of opening a 
>>>> Category Theory community group, which would allow people 
>>>> interested in CT to have a space to talk about how it 
>>>> applies to web standards, from RDF, SPARQL, Property Graphs,
>>>> etc... all the way to HTTP. This could attract mathematicians 
>>>> and allow them to see which other groups could be helped 
>>>> from some theoretical input, write up a wiki of concepts
>>>> and papers that are related, and a lot more….
>>>> 
>>>> Feedback welcome :-)
>>>> 
>>>>> On 23 Sep 2019, at 15:08, ProjectParadigm-ICT-Program <metadataportals@yahoo.com> wrote:
>>>>> 
>>>>> Good. Finally we are starting to see the light. But an even more generalized model is possible, because the essence here is representing data, whereas there are two more levels, i.e. information and knowledge. And both can also be captured using category theory and formal algebra, but with a twist.
>>>> 
>>>> Yes, I agree. Knowledge involves modal concepts (at least Nozick’s definition
>>>> in Philosophical Explanations gave some very good reason to believe so).
>>>> 
>>>> I recently discovered that an introductory book on Modal HoTT (for philosophers) 
>>>> was to come out soon. In the already published chapter 4 is written there that
>>>> 
>>>> "The slogan here is that, where HoTT itself is the internal language of (∞,1)-toposes, modal HoTT is the internal language for collections of (∞,1)-toposes related by geometric morphisms”
>>>> 
>>>> This brings a whole new level of mathematical clarity to the subject.
>>>> I wrote up a blog post to help me read that article with pointers to articles
>>>> and research here:
>>>> 
>>>> ”Modal HoTT on the Web"
>>>> https://medium.com/@bblfish/modal-hott-on-the-web-2f4f7996b41f
>>>> 
>>>> Henry
>>>> 
>>>>> 
>>>>> Milton Ponson
>>>>> GSM: +297 747 8280
>>>>> PO Box 1154, Oranjestad
>>>>> Aruba, Dutch Caribbean
>>>>> Project Paradigm: Bringing the ICT tools for sustainable development to all stakeholders worldwide through collaborative research on applied mathematics, advanced modeling, software and standards development
>>>>> 
>>>>> 
>>>>> On Monday, September 23, 2019, 9:10:16 AM ADT, Henry Story <henry.story@bblfish.net> wrote:
>>>>> 
>>>>> 
>>>>> Hi,
>>>>> 
>>>>> An interesting paper linking knowledge graphs, property graphs and 
>>>>> RDF together via Category Theory
>>>>> 
>>>>> Algebraic Property Graphs
>>>>> https://arxiv.org/abs/1909.04881
>>>>> 
>>>>> Henry Story
> 
> -- 
> Hugh
> 023 8061 5652
> 
>

Received on Thursday, 14 November 2019 12:45:41 UTC