August 26th Meetup

[Tim McGilchrist]

Welcome to another month of tasty FP talks. This month we have two talk on offer and will be doing things online. Being online is super helpful this month because we have a new speaker Jack Kelly from Brisbane, welcome Jack and thanks for joining us. After Jack we have

a long term FP-SYD member and all round fantastic guy Mark Hopkins giving us a talk on Topos Theory. Longer abstracts for both talks below.

As always we have a slack channel, leave a message here and an invite link can be yours!

Note you need to RSVP to see the zoom link and I'll be recording talks as well.

On the recordings, I've setup a YouTube channel and am working through editing the last few months worth of talks. 

Cheers,

FP-SYD Organisers

-----------------------------------------------------------------------

contraints-extras - Jack Kelly

My talk will introduce the motivation for constraints-extras by showing a problem you bump into with libraries like dependent-sum, and build up all the necessary machinery from dependent-sum and constraints such that people don't need to be familiar with the underlying libraries to follow along.

-----------------------------------------------------------------------

A Taste of Topos Theory - Mark Hopkins

There are many ways to approach the mathematical field of topos theory.

One view is that the concept of "topos" allows us to extract an interface

from set theory, that we can apply to other domains that also fit the definition of a topos.

The interface turns out to be a lambda calculus, and one with a lot of nice

features: it has sums and products, it's dependently typed, it has refinement types with intersection and union i.e. we can form subtypes by applying a predicate, and frequently it comes with other goodies like modalities.

By happy coincidence some of the most common constructions in discrete maths and computer science - graphs, automata - are topoi, or at least quasitopoi.

We'll explore what this all means with an example or two.