That's not ~~intuitive~~ intuitionistic

w.hs

{-

@lexi_lambda (at twitter)
https://mobile.twitter.com/lexi_lambda/status/1192930938537332736?s=19



-}

{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -fdefer-typed-holes #-}

class Functorish f where
  -- We don't need to care if it's a valid Functor or not.
  mappish :: forall a b. (a -> b) -> f a -> f b

data T = NeverNeverEverUseThisConstructor T

-- The question is whether `goal` is possible to write.
goal :: forall f a b. (Functorish f) => ((T -> a) -> b) -> (T -> f a) -> f b
goal = _

-- It's not always impossible. For example, if we *knew* T is inhabited,
t :: T
t = _

goal1 :: forall f a b. (Functorish f) => ((T -> a) -> b) -> (T -> f a) -> f b
goal1 f g = mappish (\a -> f (const a)) (g t)

-- But if T is not inhabited, i.e. T is isomorphic to Void,
--     ((T -> a) -> b) -> (T -> f a) -> f b
--   ~ ((Void -> a) -> b) -> (Void -> f a) -> f b
--   ~ (() -> b) -> () -> f b
--   ~ b -> f b
--
-- It turns out we need (purish :: ∀b. b -> f b) too, but it is not provided.
--
-- This answers the initial question: it's not always possible.
-- Probably I may stop here, but let's delve into more!

-- As said, if we had the following function for `f`,
class Functorish f => Pointy f where
  purish :: forall b. b -> f b

-- And we knew T is not inhabited,
not_t :: T -> a
not_t = _

-- We can have `goal`.
goal2 :: forall f a b. (Pointy f) => ((T -> a) -> b) -> (T -> f a) -> f b
goal2 f _ = purish (f not_t)

-- Combining above, if we knew T is either inhabited or not,
-- then we have implementation for `f`.

data Question t a = ToBe t | NotToBe (t -> a)
type ExcludedMiddle t = forall a. Question t a
excludedMiddleForT :: ExcludedMiddle T
excludedMiddleForT = _

goal3 :: forall f a b. (Pointy f) => ((T -> a) -> b) -> (T -> f a) -> f b
goal3 f g = case excludedMiddleForT of
  ToBe t        -> mappish (\a -> f (const a)) (g t)
  NotToBe not_t -> purish (f not_t)

-- Is it possible to define `Pointy` version of the goal
-- without requiring any constraint on `T`?
--
-- The answer is no. There is a known fact that we can't
-- write a program which implements:
--   excludedMiddle :: forall t. ExcludedMiddle t
--
-- But we can define it using our goal!
-- Our goal is as powerful as `excludedMiddle`, which is
-- known to be impossible.

instance Functorish (Question t) where
  mappish f (ToBe t)        = ToBe t
  mappish f (NotToBe not_t) = NotToBe (f . not_t)

instance Pointy (Question t) where
  purish b = NotToBe (const b)

goal' :: forall f t a b. (Pointy f) => ((t -> a) -> b) -> (t -> f a) -> f b
goal' = _

excludedMiddle :: forall t. ExcludedMiddle t
excludedMiddle =
  case goal' id ToBe of
    ToBe t -> ToBe t
    NotToBe f -> NotToBe (\t -> f t t)