An idea to extend the proc-syntax-ness of Agents

[freckletonj]

Thanks for the help on Stackoverflow today! I've really been enjoying getting to know your library, and in conjunction, learning tradeoffs between your approach and that of Conal Elliot in concat, namely, his objects look more like type Object k :: * -> Constraint. (If you know of any literature, discussion group threads etc on the tradeoffs between the 2 approaches, please let me know!)

Anyway, I wanted to share an extension to Agents I've been playing around with that makes it act a little more like proc syntax, namely, allowing for tuples of GenericAgents. It's messy, I could probably simplify it, but, it works!:

type O4 p a b c d = (Object p a, Object p b, Object p c, Object p d)
type O6 p a b c d e f = (Object p a, Object p b, Object p c, Object p d, Object p e, Object p f)

-- | Interpret tuples of 'GenericAgent' as just a 'GenericAgent'.
class AgentParam p q b where
  type AgentParamC p q b :: Constraint
  type AgentParamOutTy p q b
  agentParam :: AgentParamC p q b => b -> GenericAgent p q (AgentParamOutTy p q b)

instance AgentParam p q (GenericAgent p q a1, GenericAgent p q a2) where
  type AgentParamC p q (GenericAgent p q a1, GenericAgent p q a2)
    = (O4 p q a1 a2 (a1, a2), PairObjects p a1 a2, PreArrow p)
  type AgentParamOutTy p q (GenericAgent p q a1, GenericAgent p q a2)
    = (a1, a2)
  agentParam (x, y) = GenericAgent (runGenericAgent x &&& runGenericAgent y)

instance AgentParam p q (GenericAgent p q a1, GenericAgent p q a2, GenericAgent p q a3) where
  type AgentParamC p q (GenericAgent p q a1, GenericAgent p q a2, GenericAgent p q a3) =
    (O6 p q a1 a2 a3 (a2, a3) (a1, (a2, a3)), PairObjects p a2 a3, PairObjects p a1 (a2, a3), PreArrow p)
  type AgentParamOutTy p q (GenericAgent p q a1, GenericAgent p q a2, GenericAgent p q a3) =
    (a1, (a2, a3))
  agentParam (x, y, z) = GenericAgent (runGenericAgent x &&& runGenericAgent y &&& runGenericAgent z)

-- | Arrow-like interface
f $-< x = f $~ agentParam x   -- hm... this is tough to type

This allows syntax like:

let       out = SomeArr <<< WowArr $-< (x, y)

     vs

proc ...  out <- SomeArr <<< WowArr -< (x, y)

This allows tupling on the input side. Then on the output side, it'd be nice if we could pattern match, like proc syntax can, so, I'm wondering if I could do something with PatternSynonyms there too, but, haven't gotten around to it yet.

Anyway, just wanted to let you know, and if this is interesting or deserves pursuit, lmk, I'd be happy to contribute a PR!

[leftaroundabout]

Thanks for the input. I'll have a look when I have more time.

[leftaroundabout]

Oh, I seem to to have been completely forgotten about this issue...

Could you give some a bit more concrete / complete example of what you want this for? The main point of agents, as I conceived them, was to avoid needing any specially arrow-y syntax and instead just Haskell lambdas which happen to work on agent-values, as a poor-man's Compiling To Categories mechanism.

I thought about something more like -XArrows arrow syntax at various points, but always found that it made more sense to just use *** and &&& directly in those cases.

[freckletonj]

No worries! My impression of Agent, and I could be wrong, wat that it recreates portions of proc syntax. I find I still struggle to think in terms of point-free arrows and proc-syntax comes more naturally. For those instances, I found I could get a poor-man's proc syntax, eg something like:

-- Agent
f = algob
  (\a -> let
      b        = myArrow   $~ a
      Pair c d = someArrow $~< (a, b, a, b)
      in thisArrow         $~ Pair c d
  )

-- Proc
f = proc a -> do
      b        <- myArrow   -< a
      (c, d)   <- someArrow -< (a, b, a, b)
      thisArrow             -< (c, d)

Using PatternSynonyms I could write Pair to un/tuple agents. I never figured out how to do sum types, or conditionals like ArrowChoice.

I went a ways with this and then realized that it's inefficient. When I use a let bound agent, I think it re-executes at every call-site. So, I think we'd need a... let primitive? or just a helper function? to keep going down this route.

It could be an interesting approach though too if it works because it could give you more control over what it "desugars to", I mean, compared to proc syntax.

I have paused this approach though, because I suspect that learning to write point-free is a skill that will come with practice, and I could potentially trust that more than the buggy stuff I was doing to Agents :D

[leftaroundabout]

Your impression is largely correct. In fact, my first idea before I implemented the Agent classes was to tap into proc syntax, but I couldn't figure out a good way to do it. Maybe you've just found that.

Hm... your proposed syntax looks intriguing, but the instances / signatures are rather scary. Maybe something like this would be more reasonable – basically inverting the type inference, compared to what you suggest:

type family AgentUnpack k c a where
  AgentUnpack k c () = ()
  AgentUnpack k c (x,y) = (AgentUnpack k c x, AgentUnpack k c y)
  AgentUnpack k c (x,y,z) = (AgentUnpack k c x, AgentUnpack k c y, AgentUnpack k c z)
  ...
  AgentUnpack k c a = Agent k c a

agentParam :: AgentUnpack k c a -> Agent k c a   -- plus some typeclass constraint
($-<) :: k a b -> AgentUnpack k c a -> Agent k c b

Perhaps it could even be

pattern AP :: AgentUnpack k c a -> Agent k c a

Would that fit the bill?

[leftaroundabout]

(This would still require a type class that might get pretty hairy.)

[leftaroundabout]

...Actually your Pair pattern synonym already looks like it would do most of the job. Would it be enough to just have concrete Pair / Triple / ... synonyms and nothing else?

[freckletonj]

Ya, Pair and the typeclass were 2 different approaches to the same problem, and could work, but, I'm not totally convinced it's the right design yet. It may be, just, I'm not sure.

As of now, my efforts here have been a little messy. For instance it relies on singletons to line up types within agents, and, I think singletons would be a non-starter. Though I think it could be rewritten to not need singletons. I just used em because I had em lying around and they helped me with some of the proofs. Here's what parts of this approach look like right now:

matchPair :: forall p q a b. (SingI a, SingI b, SingI q, PreArrow p, ProveObj p, ProvePair p) => GenericAgent p q (a, b) -> (GenericAgent p q a, GenericAgent p q b)
matchPair ga = (GenericAgent a, GenericAgent b) where
  tup = runGenericAgent ga
  a = proveObj @p (sing @a) (
      proveObj @p (sing @b) (
      proveObj @p (sing @q) (
      proveObj @p (SPair (sing @a) (sing @b)) (
      provePair @p (sing @a) (sing @b) (
          tup >>> fst
      )))))
  b = proveObj @p (sing @a) (
      proveObj @p (sing @b) (
      proveObj @p (sing @q) (
      proveObj @p (SPair (sing @a) (sing @b)) (
      provePair @p (sing @a) (sing @b) (
          tup >>> snd
      )))))


-- Note: Pattern Synonyms:
--   https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms
--   https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/pattern_synonyms.html
pattern Pair :: forall p q a b. (SingI a, SingI b, SingI q, PreArrow p, ProveObj p, ProvePair p) => GenericAgent p q a -> GenericAgent p q b -> GenericAgent p q (a, b)
pattern Pair a1 a2 <- (matchPair -> (a1, a2)) where -- pattern matching half
        Pair a1 a2 = agentParam (a1, a2)            -- constructor half

I think the piece I was missing to get the proofs written without singletons was solved by Conal's HasCon and OpCon, though, I don't fully understand what's going on there yet.

So, the issues I'm aware of with this approach are:

• make sure the design is a good design
• can we handle sum types? or at least have an ifThenElse operator, or cond operator?
• can we improve sharing, via perhaps a let primitive/function

With those things solved, I think this would be a viable alternative to proc syntax, and perhaps be relevant in the broader community for replacing proc!

[leftaroundabout]

Really, there are two bigger issues underlying here:

1. Always carrying around the constraints for objects and pairs of them is a pain. I'm not sure what HasCon / OpCondoes to help there... have a hard time grokking that too.
2. What even is an agent? If it's just GenericAgent then it seems dubious why this is even needed, since this is nothing but a newtype-wrapped morphism that could as well be used/composed as it is. The main thing that the HasAgent interface currently does is allowing the type of the original argument to be hidden (through the rank-2 type of alg). That's how I always thought about it: an agent is a way to “view” the result of a morphism without thinking about the arguments. Specifically, it allows defining mathematical functions in the common x^2 + sin (x/2) style, hiding the fact that x isn't really any particular real value but a free variable. This does under the hood involve grouping together values, but the tuples never explicitly mentioned or split up like you want. Perhaps the Agent approach is just not suitable to this.

More practically, a problem I see with your Pair is that it duplicates the entire morphism, from the start. E.g. you end up doing

(f <<< expensiveComputation) &&& (g <<< expensiveComputation)

instead of

(f&&&g) <<< expensiveComputation

This could perhaps be avoided with rewrite rules, but better would be to not let it come to that in the first place.

As for ifThenElse: well, choose is how I addressed that. Are you asking about something that can't be expressed with choose, or just about nicer syntax for it?