Open freckletonj opened 2 years ago
Thanks for the input. I'll have a look when I have more time.
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.
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
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?
(This would still require a type class that might get pretty hairy.)
...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?
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:
ifThenElse
operator, or cond
operator?let
primitive/functionWith 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!
Really, there are two bigger issues underlying here:
HasCon
/ OpCon
does to help there... have a hard time grokking that too.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?
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 liketype 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
Agent
s I've been playing around with that makes it act a little more like proc syntax, namely, allowing for tuples ofGenericAgent
s. It's messy, I could probably simplify it, but, it works!:This allows syntax like:
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 withPatternSynonym
s 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!