Skip to content

Decidable should not depend on Divisible #64

Description

@Zemyla

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions