{-# LANGUAGE FunctionalDependencies #-}

-- | Pattern matching type class for the pattern @p@ and its cases @c@.
--
-- Additionally:
--
-- 1. @m@ can be used to limit @p@ and @b@ to same category @k@.
--
-- 2. In comparison, @c@ is left alone, to give the flexibility of how it is related to @m p@ to their
-- 'PatternMatchable' instance. For example, a @m BOOL@ might prefer @c = Bool@, instead.
class PatternMatchable m p c k | m -> k, m p -> c where
  -- | Create the pattern @m p@ in the case of @c@.
  inCase :: forall. c -> m p

  -- | Match pattern @m p@ with case analysis function @c -> m b@ that returns a @m b@.
  --
  -- In many cases, it is not possible to construct: @fromCases :: forall. m p -> c@.
  -- However, applying the yoneda embedding @forall x. (a -> x) -> (b -> x) ≅ b -> a@,
  -- then we have: @(c -> m b) -> (m p -> m b) ≅ m p -> c@.
  --
  -- The'match' function flips the arguments from yoneda embedding for the syntactical reason:
  -- @mach p (\c -> case c of -> _)@
  match :: forall b. k b => m p -> (c -> m b) -> m b

{- An example application:

maybe_foo2 = fn @(Maybe U32 -> Maybe U32 -> U32) "maybe_foo2" $
  \x1 x2 -> match (x1 + x2) \case
    Just r  -> r
    Nothing -> 0

foo2 = fn @(U32 -> U32 -> U32) "foo2" $
  \x1 x2 -> call'p maybe_foo2 (inCase (Just x1)) (inCase (Just x2))

-}

main = do
  print "okay"