Dear Kim, This was not intended as caricature at all. But it seems an excellent example of x-y problem indeed. When asking for a real life examples, I provided a case when I can provide example that is familiar to most readers: T = Types i = infer :: object -> type c = check :: type -> object -> Bool Laws just make sure that type checking is preserved over unification or anti-unification (<>), except for commutativity - which is omitted on purpose (further description here: https://arxiv.org/abs/2011.03076.) Naturally this example just enumerates the laws that are true for both unification and anti-unification problems. Your question would be however fitting for ICFP 2021 trivia, since without examples provided by other haskell-cafe readers I would not have guessed that you want to mean "occlusion", instead of magic of "occult" here. On Thu, Nov 12, 2020 at 2:33 AM Kim-Ee Yeoh <ky3@atamo.com> wrote:
(I'll respond with the original subject heading and with the full thread of Michal's reply copied below so that the convo stays in one place.)
Hi Michal, I'm afraid you caricaturize my original email out of proportion here:
class Monoid m => T m o where i :: o -> t c :: t -> o -> Bool <snip>
(...)
On Wed, Nov 11, 2020 at 8:36 PM Michal J Gajda <mgajda@mimuw.edu.pl> wrote: (...)
Such that the following laws are satisfied:
Forall x y z m n. c (i x) x =True c mempty x = False c m y = True => c (m <> n) y = True c n y = True => c (m <> n) y = True
What does it tell you about the definitions? Can you tell if this set of laws is correctly stated or exhaustive? Whether it models what I intend to do? Without further examples could I claim that it may be universal model for some phenomena f and g? -- Cheers Michał