[Feature Request] Extend `==*` to represent `×`.

[NoahStoryM]

See previous discussion here: https://github.com/drym-org/qi/pull/61

Here are some examples and rules that I believe useful: (from section 6.5.1 of Category Theory for Computing Science)

#lang racket

(require qi)

(define add (procedure-reduce-arity + 2))
(define mul (procedure-reduce-arity * 2))
(define id  (procedure-reduce-arity values 1))

;; f(x, y) = x^2 + 3xy.

;; λ Calculus style
(define f (λ (x y) (add (mul x x) (mul (mul x y) 3))))

;; Cartesian Closed Categories style
(define f
  (☯ (~> (-< 1> 1> 1> 2> 3)  ; x x x y 3
         (==* mul   mul   id) ; x*x x*y 3
         (==* id    mul)      ; x*x x*y*3
         (==* add))))         ; x*x+x*y*3
;; (==* f) is f
;; (==*) may map (values) to (values) ?

;; rules among `~>`, `-<` and `==*`
;; `==` is just a special case of `==*`
(-< (~> u f) (~> v g))     ; (-< (~> u f) (~> v g))
(~> (-< u v) (==* f g))     ; (~> (-< u v) (== f g))

(==* (~> f1 g1) (~> f2 g2)) ; (== (~> f1 g1) (~> f2 g2))
(~> (==* f1 f2) (==* g1 g2)) ; (~> (== f1 f2) (== g1 g2))

(-< f g)                   ; (-< f g)
(~> (==* _ _) (>- f g))     ; (~> (==* id id) (== f g))

[NoahStoryM]

In addition, I think the theoretical basis of qi (free-point) should be the Cartesian Closed Category (CCC).

Of all the advantages of cartesian closed categories, the most important is that there being no variables, we never have to worry about any clash of variables.

[NoahStoryM]

From a category point of view, (~> f g) is g∘f, (-< f g) is <f,g>, so I guess >- should probably be seen as the dual of -<, i.e. (>- f g) is <f|g>, not f×g. Perhaps extending ==* to use (==* f g) to represent f×g is more appropriate.

[countvajhula]

From a category point of view, (~> f g) is g∘f, (-< f g) is <f,g>, so I guess >- should probably be seen as the dual of -<, i.e. (>- f g) is <f|g>, not f×g. Perhaps extending == to use (== f g) to represent f×g is more appropriate.

Cartesian closed category certainly sounds very relevant, I'm glad you brought it up. I'm not familiar with this notation though (or category theory, especially) -- what do you mean by f×g here, and what would you expect (==* f g) to produce in this case, for instance, in your above example? If f×g is component-wise application of f and g, then I think (== f g) is already that, no?

My first reaction to the example is that it could be simplified by introducing generalized versions of group and bundle, i.e. having the same relationship to those forms as partition does to sieve. That could allow something like:

(define-flow f
  (~> (-< 1> 1> 1> 2> 3)        ; x x x y 3
      (collate [2 mul] [2 mul]) ; x*x x*y 3
      (group 1 id mul)          ; x*x x*y*3
      add))

... where collate is something like (group n0 f0 (group n1 f1 ...)).

Would that achieve what you had in mind?

i.e. (>- f g) is <f|g>

Do you mean a "sum type" where the output is either f or g applied to the input? That could be interesting, something like "the first function that works"?

It could make sense to try functions sequentially until there is any output (vs zero output), similar to the current implementation of Maybe in the docs. A kind of pure values-based (instead of exception-based) try. I like this idea! We'd have to find practical uses of it before including it in the language though (probably not hard to find - e.g. (~> (user) (new-try auth-using-fingerprint auth-using-drivers-license auth-using-facial-recognition) visit-account-page)).

[NoahStoryM]

I'm not familiar with this notation though (or category theory, especially) -- what do you mean by f×g here, and what would you expect (==* f g) to produce in this case, for instance, in your above example?

Yes.

If f×g is component-wise application of f and g, then I think (== f g) is already that, no?

== is very similar to ×, I noticed that some identities specified in the 8.7 documentation are also the properties of × in the category theory. Except that == only uses single-argument functions.

[edit]: For example, if there are f : A × B -> X and g : C × D -> Y, then f×g : A × B × C × D -> X × Y.

Would that achieve what you had in mind?

Using group looks good! And I want to point out that it may be important to keep qi's operators as consistent as possible with category theory's (since some programmers are more familiar with them). The rules I proposed above should also work for the ==* I expect. If we use group or collate instead, there should be some formulas, but these formulas may not look as elegant as in category theory.

Do you mean a "sum type" where the output is either f or g applied to the input?

Yes, I think Sum is useful when building typed/qi in the future. The current qi mainly deals with values (Cartesian product), and some operators may have their dual (Sum):

|-----------------------+------------------------|
| Qi                    | Category Theory        |
|-----------------------+------------------------|
| (~> f g)              | g∘f                    |
| (==* f g) / (==+ f g) | f×g        / f+g       |
| (-< f g)  / (>- f g)  | <f,g>      / <f|g>     |
| △        / ◁        | *->product / *->sum    |
| ▽        / ▷        | product->* / sum->*    |
| ⏚         / ≂         | *->1       / 0->*      |
| n>        / n<        | proj_n     / inj_n     |
| fanout    / fanin     | <id,id,…>  / <id|id|…> |
| ><        / <>        |                        |
|-----------+-----------+------------------------|

[NoahStoryM]

If qi supports dual of values (named covalues), perhaps there is no need to use conditionals in flow.

For example:

(define string->symbol/list
  (λ (str sym?)                          ; str × (t ∪ f)
    (if sym?
        (string->symbol str)
        (string->list   str))))

;;  t : #t
;;  f : #f
;;  1 : (values)
;;  d : (A×B)+(A×C) -> A×(B+C)
;; ¬d : A×(B+C) -> (A×B)+(A×C)
(define string->symbol/list
  (☯                                     ; str × (t ∪ f)
   (~> (==* id bool->1+1)                ; str × (1 + 1)
       ¬d                                ; str + str
       (==+ string->symbol string->list) ; sym + lst
       (>- id id))))                     ; sym ∪ lst

And I realize that covalues does not need to depend on a type system. I have a rough idea of how to implement it. I will open an issue to discuss it when I figure it out.

[NoahStoryM]

Here's an interesting truth table example from section 5.7.7 of Category Theory for Computing Science:

;; Truth Table

#|
  |-------+----|
  | #t #t | #t |
  | #t #f | #f |
  | #f #t | #f |
  | #f #f | #f |
  |-------+----|
|#

(define f
  (☯
   (~> (==+ (>- #t #f) (>- #t #f))
       (==+ (-< #t id) (-< #f id))
       (>- _ _))))

(~> () 1< f)  ; (values #t #t)
(~> () 2< f)  ; (values #t #f)
(~> () 3< f)  ; (values #f #t)
(~> () 4< f)  ; (values #f #f)

(~> (#t #t) ¬f)  ; 1<
(~> (#t #f) ¬f)  ; 2<
(~> (#f #t) ¬f)  ; 3<
(~> (#f #f) ¬f)  ; 4<

(~> (#t #t) ¬f (>- #t #f #f #f))  ; #t
(~> (#t #f) ¬f (>- #t #f #f #f))  ; #f
(~> (#f #t) ¬f (>- #t #f #f #f))  ; #f
(~> (#f #f) ¬f (>- #t #f #f #f))  ; #f

[benknoble]

As a category theory novice, much of this is a bit over my head, so being categorically consistent isn't as important to me as "making sense" for some intuitive notion of what that sense is. Of course, to some, being categorically consistent is making sense. But for the rest of us, Qi needs to feel consistent and sensible without the most abstract branch of mathematics :)

With that in mind, I would like to propose trying to distinguish between the "categorical underpinnings" of Qi and the "everyday programmer's" Qi. It seems like the former arose out of @countvajhula's desire to work more elegantly with values, but I may be wrong here. The latter seems to have arisen out of natural discovery and exploration with what, exactly, Qi might represent in a categorical sense.

I like the idea that the two forms of Qi above feed off of each other, but I hesitate to get too categorical (or too pedestrian!) lest we lose what I love about Qi: the expression of (some) computations more naturally than in plain Racket. [If writing Qi became an exercise in categorical maths, or if Qi's semantics broke intuitive and categorical laws, I'm sure none of us would be happy.]

Lastly, I would probably benefit from seeing some of these ideas implemented and seeing realistic computations expressed through them. This is easy to do as a library, with @countvajhula's excellent notion of extensible Qi!

[NoahStoryM]

As a category theory novice, much of this is a bit over my head, so being categorically consistent isn't as important to me as "making sense" for some intuitive notion of what that sense is. Of course, to some, being categorically consistent is making sense. But for the rest of us, Qi needs to feel consistent and sensible without the most abstract branch of mathematics :)

I'm not very good at category theory either. When I was studying category theory, I kept thinking about whether some constructs could be transformed to programming languages. After a few days of research, I found that Qi's design is surprisingly consistent with the computational style of category theory. I think this is because the values handled by Qi is exactly the Cartesian Product. And in my personal experience, mapping mathematics into programming is likely to help us find a natural way of thinking about the problem. After that, we only need to introduce this new perspective to new users, without telling them the mathematics behind it (if they are not interested).

And Qi is already highly consistent with category theory (such as (-< f g) and <f,g>), which also reflects the deep connection between them. The only exception is the product of functions ((==* f g) and f×g), which is exactly what this issue hopes Qi can improve (the * in ==* can represent the product, it's a surprise for me!), I guess the first example (f(x, y) = x^2 + 3xy) should clarify the usages of f×g, which may not be too hard for programmers to understand and use.

The latter seems to have arisen out of natural discovery and exploration with what, exactly, Qi might represent in a categorical sense.

@countvajhula expressed confusion about the meaning of some missing shapes (like <>). At the moment I think what is really missing is the duality of values (covalues)​​. I found that some sum-related constructs in category theory can be described via Qi (and surprisingly fit!) if covalues is supported. It even helped me further understand what I had learned in the past!

With that in mind, I would like to propose trying to distinguish between the "categorical underpinnings" of Qi and the "everyday programmer's" Qi. It seems like the former arose out of @countvajhula's desire to work more elegantly with values, but I may be wrong here.

The string->symbol/list and truth table examples I gave before seem to confuse the normal programmer because of covalues. I'm trying to implement covalues and figure out some details, and I'll introduce covalues in detail after that. I believe Qi programmers will enjoy covalues after understanding it!

Lastly, I would probably benefit from seeing some of these ideas implemented and seeing realistic computations expressed through them. This is easy to do as a library, with @countvajhula's excellent notion of extensible Qi!

Personally, I hope that Qi's operators can be as consistent as possible with category theory's (I hope ==* is isomorphic to ×), and Qi can handle covalues and support the missing shapes. Of course, if the covalues ​​I'll introduce later still confuse you, it's not bad for me to abstract covalues into another library. :)

[countvajhula]

Fwiw I'm whole-heartedly in agreement with all points of view expressed above 😄 . Too much emphasis either on abstract theory or everyday convenience could lose the best of both that could be derived from exploring each with an interest in improving the other. I don't think there will truly be a contradiction between theory and practice if we take this perspective on it, and put in the effort necessary to make theory relatable and useful, and practice precise and consistent.

After all, not every theory is valid, and especially if it deviates too far from intuition, it is likely to be in some way wrong or inapplicable, and should not be followed too dogmatically. On the other hand, intuition is sometimes mistaken, and basing it on a correct theory can then give the intuition room to grow into a more elegant way of looking at things.

I believe we're all on the same page that category theory connections should be explored to the extent that they help us understand the language and allow us to say things even more intuitively. I'm not too worried that we'll go down the path of being an esoteric mathematical language. Qi will always be about being intuitive and clear, and I am hopeful that the math will only help as long as we keep each other honest by holding each other to these standards 🙂

Now, I personally just don't understand any of this stuff yet 😅 . I'll have to spend some time looking into it - but for signposting purposes, note that Qi's main priority right now, as I see it, is the compiler work. So category theory connections will probably proceed at a slower rate, though it is very much an intriguing avenue that I think we are all interested in, so thank you @NoahStoryM for scouting the way forward on this.

On a practical note, I second @benknoble that, as language improvements can be prototyped using macros (note that the macro expansion rule has the highest priority in the flow macro, so you can override any built-in form using a macro), things like covalues and ==* could be written as Qi macros initially (not a requirement - just a recommendation) so that we can try it out and see how it feels and what benefits it has. Whether to include them in the language or not could be a longer term discussion as we learn more about the benefits and tradeoffs.

[NoahStoryM]

I have implemented sum-related operators (see https://github.com/NoahStoryM/qi-cat) successfully! I will try to write a tutorial and look for more application scenarios in the next few days. And my experience shows that qi with covalues is really amazing and elegant! 😉

[countvajhula]

Exciting, @NoahStoryM ! Looking forward to reading the tutorial and trying it out.