> ... 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.
I don't really understand. Can't you do this with type families using [`-XTypeFamilies`](https://wiki.haskell.org/GHC/Type_families) or is there some limitation I am not understanding? You might be able to get away with just a GADT.
> ...note that http://okmij.org/ftp/tagless-final/course/lecture.pdf is about representing the STLC in Haskell...
This isn't exactly right. If you read that paper carefully you see Oleg presents the Linear Lambda Calculus rather than the Simply Typed Lambda Calculus.
That paper talks about other final tagless DSLs too. My favorite DSL like this is [Servant](https://haskell-servant.readthedocs.io/en/stable/). Mestanogullari has a paper on this from [2015](https://www.andres-loeh.de/Servant/servant-wgp.pdf) if you haven't encountered it.
From what I can tell, Servant the gold standard for type driven development web development. I can talk more about this in the *Categories for the Working Hacker* discussion group if you are interested.
> Of course, you can still do a 'deep embedding' of AQL into Haskell/Java/etc, which is how AQL is actually implemented.
I am reluctant to embrace this.
Java in particular is a huge pain. Manipulating AST typically involves what the [Gang of Four](https://en.wikipedia.org/wiki/Design_Patterns) calls the "Visitor pattern". This is really hard to extend, debug and understand. Alex Miller has a nice discussion of this problem over on the [IBM developerWorks blog (2011)](https://www.ibm.com/developerworks/library/j-treevisit/index.html).
You would presumably also have to rewrite type inference and [unification](https://en.wikipedia.org/wiki/Unification_(computer_science)).
I assume you guys are doing [generative testing](https://en.wikipedia.org/wiki/QuickCheck) in lieu of real formal verification. Is there a good Java library for that?
> 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.
That matches my intuition about people.
> 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]).
Why do schema mappings need to be terms?
Couldn't they be types like how Servant has routes as types?
(We should probably take this discussion over to the Applied Category Theory Discussion Groups section).
I don't really understand. Can't you do this with type families using [`-XTypeFamilies`](https://wiki.haskell.org/GHC/Type_families) or is there some limitation I am not understanding? You might be able to get away with just a GADT.
> ...note that http://okmij.org/ftp/tagless-final/course/lecture.pdf is about representing the STLC in Haskell...
This isn't exactly right. If you read that paper carefully you see Oleg presents the Linear Lambda Calculus rather than the Simply Typed Lambda Calculus.
That paper talks about other final tagless DSLs too. My favorite DSL like this is [Servant](https://haskell-servant.readthedocs.io/en/stable/). Mestanogullari has a paper on this from [2015](https://www.andres-loeh.de/Servant/servant-wgp.pdf) if you haven't encountered it.
From what I can tell, Servant the gold standard for type driven development web development. I can talk more about this in the *Categories for the Working Hacker* discussion group if you are interested.
> Of course, you can still do a 'deep embedding' of AQL into Haskell/Java/etc, which is how AQL is actually implemented.
I am reluctant to embrace this.
Java in particular is a huge pain. Manipulating AST typically involves what the [Gang of Four](https://en.wikipedia.org/wiki/Design_Patterns) calls the "Visitor pattern". This is really hard to extend, debug and understand. Alex Miller has a nice discussion of this problem over on the [IBM developerWorks blog (2011)](https://www.ibm.com/developerworks/library/j-treevisit/index.html).
You would presumably also have to rewrite type inference and [unification](https://en.wikipedia.org/wiki/Unification_(computer_science)).
I assume you guys are doing [generative testing](https://en.wikipedia.org/wiki/QuickCheck) in lieu of real formal verification. Is there a good Java library for that?
> 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.
That matches my intuition about people.
> 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]).
Why do schema mappings need to be terms?
Couldn't they be types like how Servant has routes as types?
(We should probably take this discussion over to the Applied Category Theory Discussion Groups section).
Version 2.1.8p2
