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

Generic Functor attempt 1: IcelandJack's categorical functor proposal #46

Closed
wants to merge 4 commits into from

Conversation

solomon-b
Copy link
Owner

@solomon-b solomon-b commented Jan 24, 2024

We need a more generic version of Functor that operates at any kind and which allows us to specify the variance of all parameters it is functorial over. This would allow us to merge the Functor/Bifunctor/Trifunctor class hierarchies (and allow for way arbitrary numbers of parameters and variances). It would also help with implementing generic sequencing operations for #45.

@Icelandjack has a proposal which is based on work by Ed Kmett. It looks really close to what we need and looks relatively simple compared to other categorical functor implementations out there.

I made this MR to facilitate discussion while we workshop the idea and decide if it will work for us.

@solomon-b solomon-b self-assigned this Jan 24, 2024
@solomon-b solomon-b force-pushed the solomon/categorical-functor branch 9 times, most recently from 4c81d17 to 829270d Compare January 27, 2024 02:54
@solomon-b
Copy link
Owner Author

solomon-b commented Jan 27, 2024

With some modification we have a working Category for Nat:

type Nat :: Cat s -> Cat t -> Cat (s -> t)
data Nat source target f f' where
  Id :: Nat source target f f
  Nat :: (FunctorOf source target f, FunctorOf source target f') => (forall x. target (f x) (f' x)) -> Nat source target f f'

instance (Semigroupoid c1, Semigroupoid c2) => Semigroupoid (Nat c1 c2) where
  o :: Nat c1 c2 j k1 -> Nat c1 c2 i j -> Nat c1 c2 i k1
  c1 `o` Id = c1
  Id `o` c2 = c2
  Nat c1 `o` Nat c2 = Nat (c1 `o` c2)

instance (Semigroupoid c1, Semigroupoid c2, Category c1, Category c2) => Category (Nat c1 c2) where
  id = Id
  (.) = o

This lets us be functorial over both parameters of a bifunctor:

newtype FromBifunctor f a b = FromBifunctor (f a b)
  deriving newtype (Hask.Functor, Hask.Bifunctor)

instance (Category (Nat (->) (->)), Hask.Bifunctor f, Functor (f a), Cod (f a) ~ (->), Dom (f a) ~ (->)) => Functor (FromBifunctor f a) where
  type Dom (FromBifunctor f a) = (->)
  type Cod (FromBifunctor f a) = (->)

  map f (FromBifunctor fab) = FromBifunctor (map f fab)

instance (Hask.Bifunctor f, forall x. FunctorOf (->) (->) (f x)) => Functor (FromBifunctor f ) where
  type Dom (FromBifunctor f) = (->)
  type Cod (FromBifunctor f) = (Nat (->) (->))

  map :: (a -> b) -> (Nat (->) (->)) (FromBifunctor f a) (FromBifunctor f b)
  map f = Nat (\(FromBifunctor fax) -> FromBifunctor (Hask.first f fax))

Unfortunately deriving via fails:

deriving via (FromBifunctor (,)) instance Functor (,)
• Couldn't match type: FromBifunctor (,) b
                 with: (,) b
    arising from a use of ‘ghc-prim-0.10.0:GHC.Prim.coerce’

And I'm still having lot of trouble using instances like map :: (a -> b) -> Nat (->) (->) ((,) a) ((,) b)

@solomon-b solomon-b force-pushed the solomon/categorical-functor branch 4 times, most recently from f0596f5 to a41cbb2 Compare January 29, 2024 21:37
@solomon-b
Copy link
Owner Author

solomon-b commented Jan 29, 2024

I've fleshed this out quite a bit, we are going to need to come up with a nicer API on top of this machinery but if I can solve a few more issues then I think its going to work for us.

We now have working Bifunctors, Profunctors, and Witherable.

I had to drop the Id constructor and the existential constraints from Nat:

type Nat :: Cat s -> Cat t -> Cat (s -> t)
data Nat source target f f' where
  Nat :: (forall x. target (f x) (f' x)) -> Nat source target f f'

Profunctor example

newtype FromProfunctor f a b = FromProfunctor (f a b)
  deriving newtype (Hask.Functor, Hask.Profunctor)

instance (Hask.Profunctor p, FunctorOf (->) (->) (p x)) => Functor (FromProfunctor p x) where
  type Dom (FromProfunctor p x) = (->)
  type Cod (FromProfunctor p x) = (->)

  map :: (a -> b) -> Cod (FromProfunctor p x) (FromProfunctor p x a) (FromProfunctor p x b)
  map f (FromProfunctor pxa) = FromProfunctor (map f pxa)

instance (Hask.Profunctor p) => Functor (FromProfunctor p) where
  type Dom (FromProfunctor p) = Op
  type Cod (FromProfunctor p) = (Nat (->) (->))

  map :: Op a b -> Nat (->) (->) ((FromProfunctor p) a) ((FromProfunctor p) b)
  map (Op f) = Nat (\(FromProfunctor pax) -> FromProfunctor (Hask.lmap f pax))

type Profunctor :: (Type -> Type -> Type) -> Constraint
type Profunctor p = (FunctorOf Op (Nat (->) (->)) p, forall x. FunctorOf (->) (->) (p x))

lmap :: forall p a b. (Profunctor p) => (a -> b) -> forall x. p b x -> p a x
lmap f = let (Nat f') = map @_ @_ @p (Op f) in f'

rmap :: (CovariantFunctor (f x)) => (a -> b) -> f x a -> f x b
rmap = fmap

dimap :: (Profunctor p) => (a -> b) -> (c -> d) -> p b c -> p a d
dimap f g = lmap f . rmap g

Current outstanding issues

Invariance

Its unclear to me how we can encode invariant parameters.

Instance Collisions

I think we need to switch from associated types to multi-parameter typeclasses. Currently we get collisions between instances such as Contravariant Functor and Witherable.

@solomon-b solomon-b force-pushed the solomon/categorical-functor branch 3 times, most recently from efe01f0 to 9dc7284 Compare January 30, 2024 04:30
@solomon-b
Copy link
Owner Author

type (<->) :: Cat Type
type (<->) = Iso (->)

instance Functor Endo where
  type Dom Endo = (<->)
  type Cod Endo = (->)

  map :: (a <-> b) -> Endo a -> Endo b
  map Iso {..} (Endo f) = Endo (fwd . f . bwd)

invmap :: (FunctorOf (<->) (->) f) => (a -> b) -> (b -> a) -> f a -> f b
invmap f g = map (Iso f g)

okay we've got examples of 1,2, and 3 param functors with various positions covariant, contravariant, and invariant.

The next step is a nicer interface ontop of FunctorOf that is a bit easier to work with.

@solomon-b solomon-b force-pushed the solomon/categorical-functor branch 4 times, most recently from 8e7f038 to d731e34 Compare January 30, 2024 19:11
This version is nice cause it collapes `Functor` and `FunctorOf` into
one class and it prevents overlapping instances when the same domain
and co-domain can yield multiple functors.

However, it also has more difficulty with instance resolution and
requires more type ascription/application.
@solomon-b
Copy link
Owner Author

@masaeedu I've moved this project into a separate repo: https://github.com/solomon-b/kindly-functors/

@solomon-b solomon-b closed this Feb 5, 2024
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

Successfully merging this pull request may close these issues.

None yet

1 participant