Ambiguous types are no longer necessary. Proxies are used instead.

.editorconfig

@@ -0,0 +1,8 @@
+root = true
+
+[*]
+charset = utf-8
+indent_style = space
+indent_size = 4
+trim_trailing_whitespace = true
+insert_final_newline = true

.github/workflows/ci.yml

@@ -5,15 +5,15 @@ on: [push]
 jobs:
   build:
     runs-on: ubuntu-latest
-        
+
     steps:
     - name: Checkout sources
       uses: actions/checkout@v2
-    
+
     - name: Install latest Haskell Stack
       uses: actions/setup-haskell@v1.1
       with:
         enable-stack: true
-        
+
     - name: Build
-      run: stack build
+      run: stack build

monoids-in-the-categoy-of-endofunctors.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 8cc4db09b2fd89bb75338d6e6a4f2062a5d57ad3925b3632f27d52a5fc4c91d4
+-- hash: 73c8dbdf7c11bd3edb3a43f645558791b10821437430c5b2b4ba1c648be52910
 
 name:           monoids-in-the-categoy-of-endofunctors
 version:        0.1.0.0
@@ -32,8 +32,6 @@ library
       Category.Functor
       Category.Functor.Const
       Category.Functor.Identity
-      Category.Internal.Ambiguous
-      Category.Internal.Hom
       Category.Monad
       Category.Monoid
       Category.Monoidal

src/Category.hs

@@ -1,27 +1,36 @@
-module Category ( module Category
-                , module Category.Internal.Ambiguous
-                , module Category.Internal.Hom
-                ) where
+module Category where
 
-import Category.Internal.Ambiguous
-import Category.Internal.Hom
 import Data.Kind (Constraint)
 
+type family Hom :: i -> i -> k
+type instance Hom = (~>)
+
+type family (~>) :: i -> i -> *
+
+type Dom (a :: i -> j) = (~>) :: i -> i -> *
+
+data Proxy :: k -> * where
+    Proxy :: Proxy k
+
+class Category (r :: k -> Constraint) where
+    identity :: forall proxy a. r a => proxy r -> Dom r a a
+    compose :: forall proxy a b c. (r a, r b, r c) => proxy r -> Dom r b c -> Dom r a b -> Dom r a c
+
 -- | A restricted alias of `identity` which does not cause type ambiguity.
 id :: forall r a. (r ~ AnyC, Category r) => Dom r a a
-id = identity @_ @r
+id = identity (Proxy @r)
 
 -- | A restricted alias of `compose` which does not cause type ambiguity.
 (.) :: forall r a b c. (r ~ AnyC, Category r) => Dom r b c -> Dom r a b -> Dom r a c
-(.) = compose @_ @r
+(.) = compose (Proxy @r)
 
 type instance (~>) = (->)
 
 -- | The category of data types.
 instance Dom r ~ (->) => Category r where
-    identity x = x
-    compose f g x = f (g x)
-  
+    identity _ x = x
+    compose _ f g x = f (g x)
+
 -- Everything below is miscellaneous crap that doesn't have a better home.
 
 class NoC

src/Category/Applicative.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
 module Category.Applicative where
 
 import Category
@@ -7,13 +6,13 @@ import Category.Functor.Identity
 import qualified Prelude
 
 class Functor r s f => Applicative r s f where
-    pure :: (r a, s (f a)) => a ~> f a
-    ap :: (r a, r b, r (a ~> b), s (f (a ~> b)), s (f a), s (f b)) => f (a ~> b) -> f a ~> f b
+    pure :: (r a, s (f a)) => proxy r s -> a ~> f a
+    ap :: (r a, r b, r (a ~> b), s (f (a ~> b)), s (f a), s (f b)) => proxy r s -> f (a ~> b) -> f a ~> f b
 
 instance {-# OVERLAPPABLE #-} Prelude.Applicative f => Applicative r s f where
-    pure = Prelude.pure
-    ap = (Prelude.<*>)
+    pure _ = Prelude.pure
+    ap _ = (Prelude.<*>)
 
 instance Applicative r s Identity where
-    pure = Identity
-    ap (Identity f) x = f <$> x
+    pure _ = Identity
+    ap _ (Identity f) x = f <$> x

src/Category/Constraint.hs

@@ -1,9 +1,9 @@
 -- | The category of constraints.
 module Category.Constraint where
-  
+
 import Category
 import Prelude (($))
-  
+
 newtype a :- b = Sub (a => Dict b)
 
 type instance (~>) = (:-)
@@ -15,5 +15,5 @@ data Dict p where
 r \\ Sub Dict = r
 
 instance Dom r ~ (:-) => Category r where
-    identity = Sub Dict
-    compose f g = Sub $ Dict \\ f \\ g
+    identity _ = Sub Dict
+    compose _ f g = Sub $ Dict \\ f \\ g

src/Category/Functor.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
 module Category.Functor where
 
 import Category
@@ -11,39 +10,40 @@ import qualified Prelude (Functor, fmap)
 -- | 1. An endofunctor, i.e. a functor from a category to itself (`Functor cat cat f`)
 -- | 2. An endofunctor in the category of *types*, where cat can *only* be `AnyC :: * -> Constraint`.
 class (Category src, Category dest) => Functor (src :: srcKind -> Constraint) (dest :: destKind -> Constraint) (f :: srcKind -> destKind) where
-    map :: forall a b. (src a, src b, dest (f a), dest (f b)) => (a ~> b) -> f a ~> f b
+    map :: forall proxy1 proxy2 a b. (src a, src b, dest (f a), dest (f b)) => proxy1 src -> proxy2 dest -> (a ~> b) -> f a ~> f b
 
 -- | A functor from a category to itself.
-type Endofunctor cat f = Functor cat cat f
+class Functor cat cat f => Endofunctor cat f
+instance Functor cat cat f => Endofunctor cat f
 
 -- | A restricted alias of `map` which does not cause type ambiguity.
 (<$>) :: forall r s f a b. (r ~ AnyC, s ~ AnyC, Functor r s f) => (a ~> b) -> f a ~> f b
-(<$>) = map @_ @_ @r @s @_ @_
+(<$>) = map (Proxy @r) (Proxy @s)
 
 -- | A contravariant functor.
 class (Category src, Category dest) => Contravariant (src :: srcKind -> Constraint) (dest :: destKind -> Constraint) (f :: srcKind -> destKind) where
-    contramap :: forall a b. (src a, src b, dest (f a), dest (f b)) => (b ~> a) -> (f a ~> f b)
+    contramap :: forall proxy1 proxy2 a b. (src a, src b, dest (f a), dest (f b)) => proxy1 src -> proxy2 dest -> (b ~> a) -> (f a ~> f b)
 
 -- | An invariant functor.
 class (Category src, Category dest) => Invariant (src :: srcKind -> Constraint) (dest :: destKind -> Constraint) (f :: srcKind -> destKind) where
-    invmap :: forall a b. (src a, src b, dest (f a), dest (f b)) => (a ~> b) -> (b ~> a) -> (f a ~> f b)
+    invmap :: forall proxy1 proxy2 a b. (src a, src b, dest (f a), dest (f b)) => proxy1 src -> proxy2 dest -> (a ~> b) -> (b ~> a) -> (f a ~> f b)
 
 {-
 instance {-# INCOHERENT #-} Functor src dest f => Invariant src dest f where
     invmap f _ = map f
-    
+
 instance {-# INCOHERENT #-} Contravariant src dest f => Invariant src dest f where
     invmap _ f = contramap f
 -}
 
 instance {-# OVERLAPPABLE #-} Prelude.Functor f => Functor r s f where
-    map = Prelude.fmap
+    map _ _ = Prelude.fmap
 
 instance (Category src, Category dest) => Functor src dest ((->) a) where
-    map f g x = f (g x)
+    map _ _ f g x = f (g x)
 
 instance (Category src, Category dest) => Functor src dest ((,) a) where
-    map f (x, y) = (x, f y)
+    map _ _ f (x, y) = (x, f y)
 
 instance (Category src, Category dest) => Functor src dest (,) where
-    map f = Nat \(x, y) -> (f x, y)
+    map _ _ f = Nat \(x, y) -> (f x, y)

src/Category/Functor/Const.hs

@@ -11,27 +11,27 @@ reconst :: Const f a -> Const f b
 reconst = Const . getConst
 
 instance (Category src, Category dest) => Functor src dest Const where
-    map f = Nat $ Const . f . getConst
+    map _ _ f = Nat $ Const . f . getConst
 
-instance {-# OVERLAPPABLE #-} (Category src, Category dest) => Functor src dest (Const f) where
-    map _ = Const . getConst
+instance (Category src, Category dest) => Functor src dest (Const f) where
+    map _ _ _ = Const . getConst
 
-instance {-# OVERLAPPABLE #-} (Category src, Category dest) => Contravariant src dest (Const f) where
-    contramap _ = Const . getConst
+instance (Category src, Category dest) => Contravariant src dest (Const f) where
+    contramap _ _ _ = Const . getConst
 
 newtype Const2 f a b = Const2 { getConst2 :: f }
 
 instance (Category src, Category dest) => Functor src dest Const2 where
-    map f = nat2 $ Const2 . f . getConst2
+    map _ _ f = nat2 $ Const2 . f . getConst2
 
-instance {-# OVERLAPPABLE #-} (Category src, Category dest) => Functor src dest (Const2 f) where
-    map f = Nat $ Const2 . getConst2
+instance (Category src, Category dest) => Functor src dest (Const2 f) where
+    map _ _ f = Nat $ Const2 . getConst2
 
-instance {-# OVERLAPPABLE #-} (Category src, Category dest) => Functor src dest (Const2 f a) where
-    map f = Const2 . getConst2
+instance (Category src, Category dest) => Functor src dest (Const2 f a) where
+    map _ _ f = Const2 . getConst2
 
-instance {-# OVERLAPPABLE #-} (Category src, Category dest) => Contravariant src dest (Const2 f) where
-    contramap _ = Nat $ Const2 . getConst2
+instance (Category src, Category dest) => Contravariant src dest (Const2 f) where
+    contramap _ _ _ = Nat $ Const2 . getConst2
 
-instance {-# OVERLAPPABLE #-} (Category src, Category dest) => Contravariant src dest (Const2 f a) where
-    contramap _ = Const2 . getConst2
+instance (Category src, Category dest) => Contravariant src dest (Const2 f a) where
+    contramap _ _ _ = Const2 . getConst2

src/Category/Functor/Identity.hs

@@ -6,4 +6,4 @@ import Category.Functor
 newtype Identity a = Identity { getIdentity :: a }
 
 instance (Category src, Category dest) => Functor src dest Identity where
-    map f (Identity x) = Identity (f x)
+    map _ _ f (Identity x) = Identity (f x)

src/Category/Internal/Ambiguous.hs

@@ -1,9 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-module Category.Internal.Ambiguous where
-
-import Category.Internal.Hom
-import Data.Kind (Constraint)
-
-class Category (r :: k -> Constraint) where
-    identity :: forall a. r a => Dom r a a
-    compose :: forall a b c. (r a, r b, r c) => Dom r b c -> Dom r a b -> Dom r a c

src/Category/Internal/Hom.hs

@@ -1,13 +0,0 @@
-module Category.Internal.Hom where
-
-type family Hom :: i -> i -> k
-type instance Hom = (~>)
-
-type family (~>) :: i -> i -> *
-
-type Arr  (f :: i)                = ((~>) :: i -> i -> *)
-type Cod  (f :: i -> j)           = ((~>) :: j -> j -> *)
-type Cod2 (f :: i -> j -> k)      = ((~>) :: k -> k -> *)
-type Dom  (f :: i -> j)           = ((~>) :: i -> i -> *)
-type Dom2 (f :: i -> j -> k)      = ((~>) :: j -> j -> *)
-type Dom3 (f :: i -> j -> k -> l) = ((~>) :: k -> k -> *)

src/Category/Monad.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
 module Category.Monad where
 
 import Category
@@ -14,8 +13,11 @@ import Prelude (undefined)
 class (Category (Functor r r), Monoid (Functor r r) m) => Monad r m
 instance (Category (Functor r r), Monoid (Functor r r) m) => Monad r m
 
-return :: forall r m. Monad r m => Dom (Functor r r) Unit m
-return = empty @(Functor r r)
+return :: forall proxy r m. Monad r m => proxy r -> Dom (Functor r r) Unit m
+return _ = empty (Proxy @(Functor r r))
 
-join :: forall r m. Monad r m => Dom (Functor r r) (Product m m) m
-join = append @(Functor r r)
+join :: forall proxy r m. Monad r m => proxy r -> Dom (Functor r r) (Product m m) m
+join _ = append (Proxy @(Functor r r))
+
+class (Category (Endofunctor cat), Comonoid (Endofunctor cat) w) => Comonad cat w
+instance (Category (Endofunctor cat), Comonoid (Endofunctor cat) w) => Comonad cat w

src/Category/Monoid.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
 module Category.Monoid where
 
 import Category
@@ -11,10 +10,18 @@ import Data.Kind (Constraint)
 import qualified Prelude
 
 class Semigroup r m => Monoid r m where
-    empty :: Unit ~> m
+    empty :: proxy r -> Unit ~> m
 
 instance {-# OVERLAPPABLE #-} (Category r, Prelude.Monoid m) => Monoid r m where
-    empty _ = Prelude.mempty
+    empty _ _ = Prelude.mempty
 
 instance {-# OVERLAPPABLE #-} (Category (Functor r r), Prelude.Monad m) => Monoid (Functor r r) m where
-    empty = Nat \(Identity x) -> Prelude.return x
+    empty _ = Nat \(Identity x) -> Prelude.return x
+
+class MonoidalCategory cat => Comonoid cat m where
+    duplicate :: proxy cat -> Dom cat m (Product m m)
+    extract :: proxy cat -> Dom cat m Unit
+
+instance MonoidalCategory cat => Comonoid cat (m :: *) where
+    duplicate _ x = (x, x)
+    extract _ _ = ()

src/Category/Nat.hs

@@ -1,6 +1,6 @@
 -- | The category of natural transformations.
 module Category.Nat where
-  
+
 import Category
 import Data.Kind (Constraint)
 
@@ -19,5 +19,5 @@ class (forall a. c (nat a)) => NatConstraint (c :: j -> Constraint) (nat :: i ->
 instance (forall a. c (nat a)) => NatConstraint (c :: j -> Constraint) (nat :: i -> j)
 
 instance Category r => Category (NatConstraint r) where
-    identity = Nat (identity @_ @r)
-    compose (Nat f) (Nat g) = Nat (compose @_ @r f g)
+    identity _ = Nat (identity (Proxy @r))
+    compose _ (Nat f) (Nat g) = Nat (compose (Proxy @r) f g)

src/Category/Semigroup.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
 module Category.Semigroup where
 
 import Category
@@ -11,10 +10,10 @@ import Prelude (curry, uncurry)
 import qualified Prelude
 
 class MonoidalCategory r => Semigroup r m where
-    append :: Dom r (Product m m) m
+    append :: proxy r -> Dom r (Product m m) m
 
 instance {-# OVERLAPPABLE #-} (MonoidalCategory r, Prelude.Semigroup m) => Semigroup r m where
-    append = uncurry (Prelude.<>)
+    append _ = uncurry (Prelude.<>)
 
 instance {-# OVERLAPPABLE #-} (Category (Functor r r), Prelude.Monad m) => Semigroup (Functor r r) m where
-    append = Nat \(Compose x) -> Control.Monad.join x
+    append _ = Nat \(Compose x) -> Control.Monad.join x