what should my law be? - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Sandy Maguire

I'm working a modeling a hierarchy thing, with the two operations:

getFoo :: Name -> Hierarchy -> Maybe Foo
setFoo :: Name -> Foo -> Hierarchy -> Hierarchy

instance Monoid Hierarchy
Sandy Maguire

but Name might not exist in Hierarchy

Sandy Maguire

here are two laws i'd expect to hold, but which clearly are not confluent:

law getFoo n (setFoo n foo h) = Just foo

law setFoo n f mempty = mempty
Sandy Maguire

the latter seems _more_ correct, but i have no idea what sort of get/set law can hold here

Sandy Maguire

maybe it's

if getFoo n h = Just p then getFoo n (setFoo n p' h) = Just p'

TheMatten

Why is first law problematic?

Sandy Maguire

well what is the value of getFoo n (setFoo n foo mempty)

Sandy Maguire

that first one reduces to getFoo n mempty which SURELY must be Nothing

TheMatten

Ah, I see - I understood setFoo as "creates specific field when not present"

TheMatten

Then maybe getFoo n (setFoo n foo h) = foo <$ getFoo n h?

Sandy Maguire

god i love the people in this community

Sridhar Ratnakumar

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
Sandy Maguire

to follow up on this, is showing that f is a monoid homomorphism enough to show that f "doesn't do anything crazy"?

Sandy Maguire

i have these two functions, with these laws:

addChild :: ResourceName -> Hierarchy -> Hierarchy -> Hierarchy

law addChild rn r h = monoid homomorphism in h
law addChild rn r (hierarchy rn rt h) = hierarchy rn rt (h <> r)
law addChild rn r (hierarchy rn2 rt h)
    | rn /= rn2 = hierarchy rn2 rt (addChild rn r h)


removeTier :: ResourceName -> Hierarchy -> Hierarchy

law removeTier rn h = monoid homomorphism in h
law removeTier rn (hierarchy rn rt h) = mempty
law removeTier rn (hierarchy rn2 rt h)
    | rn /= rn2 = hierarchy rn2 rt (removeTier rn h)
Sandy Maguire

then i have this other law:

law removeTier rn (addChild pn (hierarchy rn rt c) h) = h

which is to show that "if you add and then remove something, nothing happens"

Sandy Maguire

which i feel like i get for free from the monoid homomorphisms...

Sandy Maguire

but then i think to myself "what if you try to add something that's already there!"

Sandy Maguire

well in that case this remove/add law is bullshit

Sandy Maguire

does this monoid exist anywhere? stupid question

newtype FirstM m = FirstM
  { unFirstM :: Alt Maybe m
  } deriving (Semigroup, Monoid, Show)

toFirstM :: m -> FirstM m
toFirstM = FirstM . Alt . Just

getFirstM :: Monoid m => FirstM m -> m
getFirstM = fromMaybe mempty . getAlt . unFirstM
Fintan Halpenny

Saw your add needs to be idempotent?

Sandy Maguire

i have been sweeping all of these issues under the rug

Sandy Maguire

with "just don't use the same ResourceName twice"

Sandy Maguire

i think i want everything to be left-biased

Sandy Maguire

the trick, i think, is to acknowledge that names are structured hierarchically

Sandy Maguire

then you only need to ensure per-tier uniqueness

Sandy Maguire

so you get the law

law (hierarchy rn rt1 c1 <> h <> hierarchy rn rt1 c2)
  = (hierarchy rn rt1 c1 <> h)
Sandy Maguire

and then

lookup [rn] h@(hierarchy rn rt c) = h
lookup (rn : rns) (hierarchy rn rt c) = lookup rns c
Sandy Maguire

that left bias makes addChild idempotent

Fintan Halpenny

Aside: Zulip on mobile is not great