Hi Matthew, you're right that the connection is between AQL and STLC, not AQL and Haskell. My presentation was about giving a semantics to the STLC using AQL; going the other way, to give a semantics to AQL using STLC/Haskell, is trickier. Let's restrict ourselves just to interpreting AQL schemas as STLC types and AQL mappings as STLC terms (the same story repeats at the level of instances). It's easy to interpret products, sums, etc of AQL schemas as products, sums, etc of STLC types. There is a problem, however, in interpreting finitely presented categories as STLC types - in particular, we need to extend the STLC with an infinite family of type constants, one for each finitely presented category (see http://categoricaldata.net/fql/fql_def.pdf), because you can't build all finitely presented categories using 0, 1, +, *, ^ alone. One alternative is to use a dependent type theory, where each finitely presented category [type constant] can be represented as a dependent type (the approach taken here: https://arxiv.org/pdf/1401.7694.pdf ). Indeed, I tried to prototype AQL in Haskell but it never really worked out due to the need for dependent types (note that http://okmij.org/ftp/tagless-final/course/lecture.pdf is about representing the STLC in Haskell, not about representing the STLC + an infinite family of constants or the STLC + dependent types in Haskell). Of course, you can still do a 'deep embedding' of AQL into Haskell/Java/etc, which is how AQL is actually implemented.

Interestingly, we found that in practice, it's actually pretty rare for people to want to use 0, 1, +, *, ^ to describe their schemas - instead, people just seem to write down specific finitely presented categories and go from there. For that reason, the only operation on schemas provided by newer versions of AQL is the colimit operation, which is very dependently typed (i.e., a colimit schema [type] is defined in terms of schema mappings [terms]).

Interestingly, we found that in practice, it's actually pretty rare for people to want to use 0, 1, +, *, ^ to describe their schemas - instead, people just seem to write down specific finitely presented categories and go from there. For that reason, the only operation on schemas provided by newer versions of AQL is the colimit operation, which is very dependently typed (i.e., a colimit schema [type] is defined in terms of schema mappings [terms]).