Construct monad in `sicp-pict`?

Oh man, there's a lot here -- this is going to be a long, multi-part response. This will cover (1) Arrows, (2) Monads in Haskell vs Qi, (3) Typed Qi.

@NoahStoryM I'm loving the thought process that went into your characterization above, thank you for sharing and for taking such care to draw diagrams.

First off, I'd love to learn more about Haskell but it is dense and I haven't had the opportunity to use it for anything before. This thread has inspired me to resume my learning of it :slight_smile:

I looked into Arrows and found this great description in the Typeclassopedia to supplement the link you sent @scolobb . I'm frankly a bit mindblown by the correspondence between Qi and Arrows here -- to me there doesn't seem to be any special reason why they ought to correspond so exactly, and yet:

  • The arr method corresponds to Qi's "base case" of treating any function as a flow.
  • (>>>) is equivalent to ~>
  • first, second, and their composite (***) is the relay -- i.e. (== a _), (== _ b), and (== a b), respectively.
  • (&&&) referred to as "fanout composition" is exactly the tee junction, (-< f g)

I suppose the reason for this close correspondence might be that, in designing these combinators, I couldn't think of any other ways to compose functions, and perhaps these really are all of the foundational (in whatever sense) ones. I did at one time also consider a "diamond" composition, <>, since it was the only shape missing in ~> -< >< ==, but I forget now what it did (or maybe I couldn't think of what it ought to do!). It probably was reducible to one of these other combinators and was not truly distinct (for that matter, while >< is reducible to == when the number of values is known, this is often not the case since the number varies at runtime -- so >< may be a distinct primitive that isn't possible in statically typed languages).

Thank you for making this connection - it is valuable! This will surely provide some clarity on the theoretical underpinnings, scope, and limitations of Qi (some of which we will return to on the subject of monads, below).

For some time now I've had the vague suspicion that some language features that are arcane in other languages could be simple in Qi (and vice versa). Arrows is clearly one of these, and I've also felt that monads would be, too, where for instance, Qi's treatment of Maybe in terms of presence or absence of values rather than annotations like Just and reified absence values like Nothing, seems to me to be more elegant (and, incidentally, this approach was inspired by buddhist sunyata logic -- what could be called "logical zero"). I suspect, but don't know for sure as my category theory is rudimentary, that this approach can generalize in a natural way to at least some other monads -- for instance, just as Maybe is presence or absence of a value, the State monad could be represented as the presence and persistence of additional values (fulfilling, of course, the necessary formal properties). IO may be the spontaneous addition of new values (functions with outputs but no inputs) in some form, and grounded side effects (functions with inputs but no outputs) that produce no values. The unifying theme here being the creation, existence or absence (and consequently also the number), and the termination of values. Of course, the monad laws would need to be proved in each case, and it would be interesting to see whether in fact every monad could be expressed in this way. If indeed Qi is Arrows, then this SO post seems to suggest that the answer is in the negative here. On the other hand, I found the original paper on Arrows, which concludes, "We have seen that any monadic library can be given an arrow interface instead (via Kleisli arrows), and so the arrow interface is strictly more general." In any case, as Qi also has a lot of features that don't necessarily reduce to the combinators discussed above, perhaps it is not "only" Arrows, and this would in that case be a theoretical lower bound on expressiveness.

To digress further on this subject, another language feature that is potentially "natural" in Qi is delimited continuations. I think in Qi they manifest simply as a "potential difference" between two points in a flow (like the concept in physics for electromagnetic fields), which is itself expressible as a flow, i.e. a function. It may be that Qi would be a good language for studying continuations as this manifestation is very natural and easy to think about -- maybe even affording a mathematical formulation that maps directly to Qi code. Just a vague idea at this stage!

Finally, returning to Typed Qi, that would indeed be an interesting project, and one that I incidentally created an issue for when you first mentioned it a little while back :slight_smile: . I recently came across this project called Turnstile that may be relevant :person_shrugging:

3 Likes