Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Decidable should not depend on Divisible #64

Open
Zemyla opened this issue Dec 7, 2019 · 3 comments
Open

Decidable should not depend on Divisible #64

Zemyla opened this issue Dec 7, 2019 · 3 comments

Comments

@Zemyla
Copy link

Zemyla commented Dec 7, 2019

Decidable seems to be, at the very least, independent of Divisible, and there's a lot of evidence that suggests that it should actually be Divisible's superclass, going backwards from Applicative/Alternative.

First off, there's the utterly unnecessary Monoid r constraint on the Decidable instance for Op r. But while that may not be convincing on its own, I have found a class that's Contravariant and Decidable but can never be Divisible:

-- Analogous to setjmp/longjmp in C, but working in a MonadCont.
newtype Jump m a = Jump { longJump :: forall x. a -> m x }

setJump :: MonadCont m => a -> m (a, Jump m a)
setJump a = callCC $ \k -> let
  j = Jump $ \b -> fmap absurd $ k (b, j)
  in return (a, j)

instance Contravariant (Jump m) where
  contramap f (Jump j) = Jump (j . f)

-- The functions here range from highly dubious to impossible, and
-- force an entirely unnecessary "Applicative m" constraint.
instance Applicative m => Divisible (Jump m) where
  -- Given what kind of functions go in Jumps, this just goes to the first value,
  -- which I guess is technically associative, but not what people expect. Also,
  -- it basically means that divide (flip (,) ()) j undefined == j.
  -- It also means that divide ((,) ()) conquer /= id, no matter what conquer is.
  divide f (Jump ja) (Jump jb) = Jump $ \c -> case f c of
    (a, b) -> ja a <*> jb b

  -- This, on the other hand, is completely undefinable, both typewise (it's
  -- basically unsafeCoerce) and semantically (where does it jump to?).
  conquer = ???

-- In contrast, the Decidable instance is perfectly well behaved and simple,
-- and requires no additional constraints.
instance Decidable (Jump m) where
  -- You just use the Jump chosen on the Left or the Right.
  choose f (Jump ja) (Jump jb) = Jump $ either ja jb . f

  -- When given a Void, it's sensible to jump into the void.
  lose f = Jump $ absurd . f

There isn't any reason to gate a sensible Decidable instance for Jump behind an impossible Divisible instance.

@fommil
Copy link

fommil commented Jul 3, 2020

isn't that Alt or Profunctor instead of Decidable? Jump looks like it's covariant rather than contravariant in m, although it is contravariant in a.

@masaeedu
Copy link

Neither should Alternative depend on Applicative, but that's a rant for a different forum.

@echatav
Copy link

echatav commented Mar 2, 2022

Logically both Applicative and Alternative should be independent and Divisible and Decidable should be independent. They correspond to the four types of Day convolution for the two categories Hask and Hask^op and their two monoidal structures with identity () and product (,) or identity Void and product Either.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants