Whoa. Curious about your hierarchy thing. Because I'm creating something similar using DMap (with polysemy DSL, which should be TH generated in the ideal world); cf. the Typed forest topic.
I'm working on the notion of (for lack of better term) "typed forests" - which is a forest type (a tree with several roots) in which each node "determines" its children types (so, dependent types?). I use GADTs to represent the node types. Each GADT constructor represents the possible choice for a n
I'm working a modeling a hierarchy thing, with the two operations:
but
Name
might not exist inHierarchy
here are two laws i'd expect to hold, but which clearly are not confluent:
the latter seems _more_ correct, but i have no idea what sort of get/set law can hold here
maybe it's
Why is first law problematic?
well what is the value of
getFoo n (setFoo n foo mempty)
that first one reduces to
getFoo n mempty
which SURELY must beNothing
Ah, I see - I understood
setFoo
as "creates specific field when not present"Then maybe
getFoo n (setFoo n foo h) = foo <$ getFoo n h
?hey BIG BRAIN PLAY
god i love the people in this community
Whoa. Curious about your hierarchy thing. Because I'm creating something similar using DMap (with polysemy DSL, which should be TH generated in the ideal world); cf. the Typed forest topic.
to follow up on this, is showing that
f
is a monoid homomorphism enough to show thatf
"doesn't do anything crazy"?i have these two functions, with these laws:
then i have this other law:
which is to show that "if you add and then remove something, nothing happens"
which i feel like i get for free from the monoid homomorphisms...
but then i think to myself "what if you try to add something that's already there!"
well in that case this remove/add law is bullshit
does this monoid exist anywhere?stupid questionSaw your add needs to be idempotent?
oh nice catch
i have been sweeping all of these issues under the rug
with "just don't use the same ResourceName twice"
i think i want everything to be left-biased
the trick, i think, is to acknowledge that names are structured hierarchically
then you only need to ensure per-tier uniqueness
so you get the law
and then
that left bias makes
addChild
idempotentSounds dope :ok:
Aside: Zulip on mobile is not great