Functor => Pointed => Applicative => Monad

[Conor McBride]

On 2 Dec 2010, at 08:04, Roman Leshchinskiy wrote:

> On 01/12/2010, at 13:04, Conor McBride wrote:
>
>> I was being slightly facetious. I was also wondering what
>> value the Pointed class would add, by asking which instances
>> of Functor would fail to be Pointed. The constantly Zero
>> (or Void, if you insist) Functor? What else?
>
> Any tuple type. Or, more generally, any multifunctor or anything  
> that carries more information than just the a.

I can see that we're not going to get

  instance Pointed ((,) a)

anytime soon, but is that the thing we'd want anyway?

Seems a bit peculiar to me, given that Pointed f basically asserts
the inhabitation of f (). Why don't we just have an Inhabited
class?

  class Inhabited x where
    something :: x

Then we can build Pointed once for all

  instance Inhabited (f ()) => Pointed f where
    pure x = fmap (uconst x) something where
      uconst :: x -> () -> x
      uconst = const

Now, write a theorem prover!

  instance Inhabited () where
    something = ()

  instance (Inhabited a, Inhabited b) => Inhabited (a, b) where
    something = (something, something)

Wouldn't that give us

  instance Inhabited a => Pointed ((,) a)

?

Or, slightly more scarily, but without an extra class

instance Pointed (Const a) => Pointed ((,) a) where
   pure b = (getConst (pure ()), b)

And we can all have fun writing Djinn in type class prolog (didn't
Oleg do that already?) until somebody points out that every type is
inhabited by bottom.

However, fun though it may be, I see no evidence yet that the game
is worth the candle.

All the best

Conor