I've long since thrown away the original AQL Haskell prototype. AQL's syntax is here: http://categoricaldata.net/fql/fql_def.pdf . Let's just focus on the syntax for schemas and schema mappings. It should look familiar, because it is 'categorical abstract machine language', extended with syntax for finite presentations of categories and functors between them. So we are basically embedded a big chunk of category theory into Haskell. The first thing we need is to somehow represent the syntax of AQL in Haskell, either as an ADT or via Conal's approach or whatever. The next step is write a denotation /evaluation function that maps each finite presentation to the category it presents (there are various approaches; in AQL, each schema denotes a decision procedure for the associated word problem of the category, rather than the category; in FQL++, each schema denotes a finite category stored as a composition table.).

After that, we would need a way to express functors between these category presentations, and to check that their action is actually functorial (this is where automated theorem proving comes in.). And finally, we need to express set-valued functors from the categories as well as implement the delta/sigma/pi data migration functors.