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

- All Categories 2.2K
- Applied Category Theory Course 323
- Applied Category Theory Exercises 149
- Applied Category Theory Discussion Groups 43
- Applied Category Theory Formula Examples 15
- Chat 468
- Azimuth Code Project 107
- News and Information 145
- Azimuth Blog 148
- Azimuth Forum 29
- Azimuth Project 190
- - Strategy 109
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 707
- - Latest Changes 699
- - - Action 14
- - - Biodiversity 8
- - - Books 2
- - - Carbon 9
- - - Computational methods 38
- - - Climate 53
- - - Earth science 23
- - - Ecology 43
- - - Energy 29
- - - Experiments 30
- - - Geoengineering 0
- - - Mathematical methods 69
- - - Meta 9
- - - Methodology 16
- - - Natural resources 7
- - - Oceans 4
- - - Organizations 34
- - - People 6
- - - Publishing 4
- - - Reports 3
- - - Software 20
- - - Statistical methods 2
- - - Sustainability 4
- - - Things to do 2
- - - Visualisation 1
- General 38

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