Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
Really curious about the best way to do isomorphism check, but with allowance for Maybe:
encodeRoute :: r -> FilePath
decodeRoute :: FilePath -> Maybe r
decodeRoute . encodeRoute = id in principle, but that Maybe is preventing us from treating this as isomorphism. What can be done here?
decodeRoute . encodeRoute = id
What's this https://github.com/hanshoglund/iso-deriving/blob/master/test/Spec.hs
data Iso α β
= Iso (α → Maybe β) (β → Maybe α)
-- | An Iso that is not necessarily surjective; as well as takes an (unchanging)
-- context value.
type PartialIso ctx s a = (ctx -> a -> s, ctx -> s -> Maybe a)
partialIsoIsLawful :: PartialIso ctx s a -> ctx -> [a] -> Bool
partialIsoIsLawful (to, from) ctx =
all $ \a -> let s = to ctx a in Just a == from ctx s
I think that paper will obviate needing a partialIsoIsLawful.
If I treat decoding routes as parsing, and encoding route as pretty-printing - that paper is super relevant to this problem.
More from Julien: https://github.com/srid/ema/issues/78#issuecomment-1036993190
Julien again, re: improving PartialIso: https://git.code.sourcephile.fr/~julm/webc/tree/main
isJust :: Maybe () <-> Bool
isJust = [biCase|
Just () <-> True
Nothing <-> False
whoa - this could be used defined bijecetive route encoders? https://hackage.haskell.org/package/invertible-0.2.0.7/docs/Control-Invertible-Monoidal.html