It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.4K
- Chat 505
- Study Groups 21
- Petri Nets 9
- Epidemiology 4
- Leaf Modeling 2
- Review Sections 9
- MIT 2020: Programming with Categories 51
- MIT 2020: Lectures 20
- MIT 2020: Exercises 25
- Baez ACT 2019: Online Course 339
- Baez ACT 2019: Lectures 79
- Baez ACT 2019: Exercises 149
- Baez ACT 2019: Chat 50
- UCR ACT Seminar 4
- General 75
- Azimuth Code Project 111
- Statistical methods 4
- Drafts 10
- Math Syntax Demos 15
- Wiki - Latest Changes 3
- Strategy 113
- Azimuth Project 1.1K
- - Spam 1
- News and Information 148
- Azimuth Blog 149
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 718

Options

Just to answer your question,

I'm not sure what question you are answering.

I think you are answering "Couldn't schema be types like how Servant has routes as types?"

the STLC forms a cartesian closed category, where the objects are types and the morphisms are terms. Similarly, the category of categories forms a cartesian closed category, where the objects are categories and the morphisms are functors. Similarly, AQL schemas form a cartesian closed category, where the objects are schemas (finitely presented categories) and the morphisms are schema mappings (morphisms of finitely presented categories). That is why it is natural to translate STLC types <-> categories and STLC terms <-> functors.

I am sorry, are you sure schemas really are the same as finitely presented categories? I thought they looked like this (taken from your website):

schema Schools = literal : Ty { entities Person School Dept foreign_keys instituteOf : Person -> School deptOf : Person -> Dept biggestDept : School -> Dept attributes lastName : Person -> String schoolName : School -> String deptName : Dept -> String }

Under the above analogy, a concrete example of a finitely presented category that I'm not sure how to represent as a Haskell type/type family/etc but I know how to represent as a Coq type, is the presentation with two objects, A and B, two generating arrows f : A -> B and g : B -> A, and the equation f.g = id.

I feel like this is a tractable problem.

*How do we represent a two object finitely presented category in Haskell?*

Please check out Conal Elliot's paper *Compiling to Categories* (2017)

You appear to want a *Constrained Category* which Conal defines in §6.

It looks like you are heavily invested in Java, so I would understand if you weren't really interested in trying Haskell.

## Comments

Yes, every finitely presented category with a decidable word problem is an AQL schema. Here is the AQL schema for {A, B, f:A->B, g:B->A, f.g=id}:

`schema S = literal : empty { entities A B foreign_keys f : A -> B g : B -> A path_equations f.g = A }`

There's a lot more you can do, like add attributes and layer the schema over a type side so that you can do things like express equations involving addition, subtraction, etc.By decidable word problem, I mean that there exists a decision procedure to decide if two morphisms are equivalent according the the path equations - in general, this problem is undecidable (it contains the word problem for groups). But AQL uses a variety of techniques from automated theorem proving to construct such procedures.

If you look at Conal's definition of category, a category is a Haskell type constructor of arity two, along with two polymorphic haskell operations:

`class Category k where id ::a‘k‘a (◦)::(b‘k‘c)→(a‘k‘b)→(a‘k‘c)`

that means that Conal's definition of category encompasses only those categories who objects are exactly the Haskell types (such as the category of Haskell types and functions, namely (->)). But the category / AQL schema S has only two objects, A and B, neither of which are Haskell types. So there's no direct way to make S into an instance of Conal's category type class.If there's a way around the issue I described above, I would very much like to learn about it.

`Yes, every finitely presented category with a decidable word problem is an AQL schema. Here is the AQL schema for {A, B, f:A->B, g:B->A, f.g=id}: <code> schema S = literal : empty { entities A B foreign_keys f : A -> B g : B -> A path_equations f.g = A } </code> There's a lot more you can do, like add attributes and layer the schema over a type side so that you can do things like express equations involving addition, subtraction, etc. By decidable word problem, I mean that there exists a decision procedure to decide if two morphisms are equivalent according the the path equations - in general, this problem is undecidable (it contains the word problem for groups). But AQL uses a variety of techniques from automated theorem proving to construct such procedures. If you look at Conal's definition of category, a category is a Haskell type constructor of arity two, along with two polymorphic haskell operations: <code> class Category k where id ::a‘k‘a (◦)::(b‘k‘c)→(a‘k‘b)→(a‘k‘c) </code> that means that Conal's definition of category encompasses only those categories who objects are exactly the Haskell types (such as the category of Haskell types and functions, namely (->)). But the category / AQL schema S has only two objects, A and B, neither of which are Haskell types. So there's no direct way to make S into an instance of Conal's category type class. If there's a way around the issue I described above, I would very much like to learn about it.`

You appear to want a

Constrained Categorywhich Conal defines in §6.`> But the category / AQL schema S has only two objects, A and B, neither of which are Haskell types. So there's no direct way to make S into an instance of Conal's category type class. > > If there's a way around the issue I described above, I would very much like to learn about it. You appear to want a *Constrained Category* which Conal defines in §6.`

It's possible something like this could work for finite categories, where you explicitly list out the composition table. But really what we want is to give a list of equations, not a composition table, since AQL schemas are not categories, they are presentations of categories (and many AQL schemas denote infinite categories, for which we can't explicitly list the composition table).

`newtype A = () newtype B = () data S :: * -> * -> * where idS :: forall X, Ok X => S X X f :: S A B g :: S B A instance ConstrainedCategory S where -- not sure how Ok works, but only A and B should be Ok id = idS o idS x = x o x idS = x o f g = idS`

`It's possible something like this could work for finite categories, where you explicitly list out the composition table. But really what we want is to give a list of equations, not a composition table, since AQL schemas are not categories, they are presentations of categories (and many AQL schemas denote infinite categories, for which we can't explicitly list the composition table). <code> newtype A = () newtype B = () data S :: * -> * -> * where idS :: forall X, Ok X => S X X f :: S A B g :: S B A instance ConstrainedCategory S where -- not sure how Ok works, but only A and B should be Ok id = idS o idS x = x o x idS = x o f g = idS </code>`

Markdown on this website is a little weird.

If you want to share a code block, it looks better if you do

`<pre>...</pre>`

rather than```` ... ````

.Conal Elliot gives examples of infinite constrained categories in §7.1, §7.4, and §7.5 of his paper.

Here is his git repository where he put the code for his paper: https://github.com/conal/concat

If you reread §6 of Conal's paper, you see he is using Bolingbroke's

constraint kindsextension.Conal cites Bolingbroke's 2011 blog post where the constraint kinds extension was announced.

If you want to use them, you might want to read the documentation.

I keep getting the feeling you aren't interested in rewriting AQL in Haskell.

That's fine, but please say so.

I also get the sense you really like Java. If so, I am jealous of you. My life as a professional programmer would be easier if I enjoyed Java, rather than merely had the strength to endure it.

(That's a little arrogant, I really

don'talways have the strength to endure it.)`Markdown on this website is a little weird. If you want to share a code block, it looks better if you do `<pre>...</pre>` rather than <code>``` ... ```</code>. > It's possible something like this could work for finite categories, where you explicitly list out the composition table. But really what we want is to give a list of equations, not a composition table, since AQL schemas are not categories, they are presentations of categories (and many AQL schemas denote infinite categories, for which we can't explicitly list the composition table). Conal Elliot gives examples of infinite constrained categories in §7.1, §7.4, and §7.5 of his paper. Here is his git repository where he put the code for his paper: https://github.com/conal/concat > `-- not sure how Ok works, but only A and B should be Ok` If you reread §6 of Conal's paper, you see he is using Bolingbroke's *constraint kinds* extension. Conal cites Bolingbroke's [2011 blog post](http://blog.omega-prime.co.uk/2011/09/10/constraint-kinds-for-ghc/) where the constraint kinds extension was announced. If you want to use them, you might want to [read the documentation](https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/constraint-kind.html). ------------------- I keep getting the feeling you aren't interested in rewriting AQL in Haskell. That's fine, but please say so. I also get the sense you really like Java. If so, I am jealous of you. My life as a professional programmer would be easier if I enjoyed Java, rather than merely had the strength to endure it. (That's a little arrogant, I really *don't* always have the strength to endure it.)`

I personally am not really interested in rewriting AQL at all, but rewriting AQL in Haskell would be a fun project for someone. Mostly I'm trying to think in advance of the challenges that would be involved, and I think there are many - the essence of AQL lies in writing down finite presentations of categories (rather than categories) and doing automated theorem proving on these presentations, and I'm not sure fancy types can make this problem go away.

`I personally am not really interested in rewriting AQL at all, but rewriting AQL in Haskell would be a fun project for someone. Mostly I'm trying to think in advance of the challenges that would be involved, and I think there are many - the essence of AQL lies in writing down finite presentations of categories (rather than categories) and doing automated theorem proving on these presentations, and I'm not sure fancy types can make this problem go away.`

I came here to learn category theory. In particular, how to leverage it better in Haskell.

If you want to help me learn, I am happy to explore AQL in Haskell. But I'll need your help, since I'm not clever enough to understand translate Java code.

I can try to fix your broken Haskell code. What's next after that? Try to do a Grothendieck construction?

`> I personally am not really interested in rewriting AQL at all, but rewriting AQL in Haskell would be a fun project for someone. I came here to learn category theory. In particular, how to leverage it better in Haskell. If you want to help me learn, I am happy to explore AQL in Haskell. But I'll need your help, since I'm not clever enough to understand translate Java code. I can try to fix your broken Haskell code. What's next after that? Try to do a Grothendieck construction?`

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.

`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.`

Hi Matthew, I wanted to let you know that Statebox is funding the development of a Haskell version of AQL, with me as one of the primary contributors. Let me know if you'd like to get involved in the effort - wisnesky@gmail.com

`Hi Matthew, I wanted to let you know that Statebox is funding the development of a Haskell version of AQL, with me as one of the primary contributors. Let me know if you'd like to get involved in the effort - wisnesky@gmail.com`