Options

FQL Discussion

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

  • 1.

    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.

    Comment Source: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.
  • 2.

    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.

    Comment Source:> 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.
  • 3.

    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

    Comment Source: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>
  • 4.
    edited June 9

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

    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 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't always have the strength to endure it.)

    Comment Source: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>&#96;&#96;&#96; ... &#96;&#96;&#96;</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.)
  • 5.

    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.

    Comment Source: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.
  • 6.

    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?

    Comment Source:> 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?
  • 7.

    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.

    Comment Source: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.
  • 8.

    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

    Comment Source: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
Sign In or Register to comment.