CoercibleFunctor.hs

{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #-}
module CoercibleFunctor where

import Prelude ()

import Data.Coerce (Coercible, coerce)

class (forall x y. Coercible x y => Coercible (f x) (f y)) => Functor f where
  map :: forall a b. (a -> b) -> f a -> f b

newtype Identity a = Identity a

instance Functor Identity where
  map f (Identity a) = Identity (f a)

newtype Wrapped f e = Wrapped (f e)

instance Functor f => Functor (Wrapped f) where
  map f (Wrapped fa) = Wrapped (map f fa)

class (forall z. Functor (p z), forall w x y z. Coercible w x => Coercible y z => Coercible (p w y) (p x z)) => Bifunctor p where
  bimap :: forall a b c d. (a -> b) -> (c -> d) -> p a c -> p b d

newtype Wrapped2 p a b = Wrapped2 (p a b)

instance Functor (p s) => Functor (Wrapped2 p s) where
  map f (Wrapped2 psa) = Wrapped2 (map f psa)

instance Bifunctor p => Bifunctor (Wrapped2 p) where
  bimap f g (Wrapped2 pac) = Wrapped2 (bimap f g pac)

class Coercible a b => Newtype a b

traverseC
  :: forall f t a
   . Coercible (f a) (f t)
  => Newtype t a
  => (a -> t)
  -> (a -> f a)
  -> t
  -> f t
traverseC _ = coerce

traverseF
  :: forall f t a
   . Functor f -- implies Coercible (f a) (f t)
  => Newtype t a
  => (a -> t)
  -> (a -> f a)
  -> t
  -> f t
traverseF = traverseC

data Either a b = Left a | Right b

instance Functor (Either a) where
  map = bimap (\x -> x)
instance Bifunctor Either where
  bimap f _ (Left a) = Left (f a)
  bimap _ g (Right b) = Right (g b)




data Mu f = In (f (Mu f))

-- This first attempt does not work because this "instance" is "missing"
-- (i.e. the magic compiler solving does not solve it like this)
-- instance (Coercible x y, Coercible (f a) (g b)) => Coercible (FreeF f x a) (FreeF g y b)

{-
data FreeF f a r = PureF a | RollF (f r)

instance Functor f => Functor (FreeF f a) where
  map _ (PureF a) = PureF a
  map g (RollF fr) = RollF (map g fr)

instance Functor f => Bifunctor (FreeF f) where
  bimap f _ (PureF a) = PureF (f a)
  bimap _ g (RollF fr) = RollF (map g fr)

newtype Free f a = Free (Mu (FreeF f a))

unFree :: Free f a -> Mu (FreeF f a)
unFree = coerce

instance Functor f => Functor (Free f) where
  map f (Free (In (PureF a))) = Free (In (PureF (f a)))
  map f (Free (In (RollF fr))) = Free (In (RollF (map (\x -> unFree (map f (Free x))) fr)))
-}

-- As a next attempt, we go through `Either` so that we can use
-- the same transitivity trick as above, since `Either` is
-- `representational` in both arguments:
newtype FreeF f a r = FreeF (Either a (f r))

-- The desired rule now holds:
-- since FreeF f x a ~ Either x (f a) ~ Either y (g b) ~ FreeF g y b
-- instance (Coercible x y, Coercible (f a) (g b)) => Coercible (FreeF f x a) (FreeF g y b)
testFreeF ::
  Functor f => Coercible a b => Coercible c d =>
  FreeF f c a -> FreeF f d b
testFreeF = coerce

instance Functor f => Functor (FreeF f a) where
  map f (FreeF x) = FreeF (map (map f) x)

instance Functor f => Bifunctor (FreeF f) where
  bimap f _ (FreeF (Left a)) = FreeF (Left (f a))
  bimap _ g (FreeF (Right fr)) = FreeF (Right (map g fr))

-- But now get stuck at `Mu`:
newtype Free f a = Free (Mu (FreeF f a))

unFree :: Free f a -> Mu (FreeF f a)
unFree = coerce

{-
testFree ::
  Functor f => Coercible a b =>
  Free f a -> Free f b
testFree = coerce
-}

{-
instance Functor f => Functor (Free f) where
  map f (Free (In (FreeF (Left a)))) = Free (In (FreeF (Left (f a))))
  map f (Free (In (FreeF (Right fr)))) = Free (In (FreeF (Right (map (\x -> unFree (map f (Free x))) fr))))
-}

-- This also gets stuck

data Freee f a = Pure a | Roll (f (Freee f a))

{-
instance Functor f => Functor (Freee f) where
  map f (Pure a) = Pure (f a)
  map f (Roll fr) = Roll (map (map f) fr)
-}