Skip to content

Instantly share code, notes, and snippets.

@ekmett
Created February 18, 2016 01:30
Show Gist options
  • Save ekmett/b26363fc0f38777a637d to your computer and use it in GitHub Desktop.
Save ekmett/b26363fc0f38777a637d to your computer and use it in GitHub Desktop.
{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}
{-# language FlexibleInstances #-}
{-# language TypeOperators #-}
{-# language ScopedTypeVariables #-}
{-# language DefaultSignatures #-}
{-# language FunctionalDependencies #-}
{-# language UndecidableSuperClasses #-}
{-# language UndecidableInstances #-}
{-# language TypeInType #-}
import qualified Data.Type.Coercion as Coercion
import Data.Type.Coercion (Coercion(..))
import qualified Data.Type.Equality as Equality
import Data.Type.Equality ((:~:)(..))
import GHC.Types (Constraint, Type)
import qualified Prelude
import Prelude (Either(..), Maybe, IO)
type Cat i = i -> i -> Type
newtype Y p a b = Y { getY :: p b a }
class Vacuous (p :: Cat i) (a :: i)
instance Vacuous p a
data Dict (p :: Constraint) where
Dict :: p => Dict p
class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->), Ob (Op p) ~ Ob p) => Category (p :: Cat i) where
type Op p :: Cat i
type Op p = Y p
type Ob p :: i -> Constraint
type Ob p = Vacuous p
id :: Ob p a => p a a
(.) :: p b c -> p a b -> p a c
source :: p a b -> Dict (Ob p a)
default source :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p a)
source _ = Dict
target :: p a b -> Dict (Ob p b)
default target :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p b)
target _ = Dict
op :: p b a -> Op p a b
default op :: Op p ~ Y p => p b a -> Op p a b
op = Y
unop :: Op p b a -> p a b
default unop :: Op p ~ Y p => Op p b a -> p a b
unop = getY
class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
type Dom f :: Cat i
type Cod f :: Cat j
fmap :: p a b -> q (f a) (f b)
class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f | f -> p q
instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) =
(FunctorOf p q f, FunctorOf p q g) => Nat { runNat :: forall a. Ob p a => q (f a) (g a) }
instance (Category p, Category q) => Category (Nat p q) where
type Ob (Nat p q) = FunctorOf p q
id = Nat id1 where
id1 :: forall f x. (FunctorOf p q f, Ob p x) => q (f x) (f x)
id1 = id \\ (ob :: Ob p x :- Ob q (f x))
Nat f . Nat g = Nat (f . g)
source Nat{} = Dict
target Nat{} = Dict
ob :: forall p q f a. FunctorOf p q f => Ob p a :- Ob q (f a)
ob = Sub (case source (fmap id :: q (f a) (f a)) of Dict -> Dict)
instance (Category p, Category q) => Functor (Nat p q) where
type Dom (Nat p q) = Y (Nat p q)
type Cod (Nat p q) = Nat (Nat p q) (->)
fmap (Y f) = Nat (. f)
instance (Category p, Category q) => Functor (Nat p q f) where
type Dom (Nat p q f) = Nat p q
type Cod (Nat p q f) = (->)
fmap = (.)
contramap :: Functor f => Op (Dom f) b a -> Cod f (f a) (f b)
contramap = fmap . unop
instance Category (->) where
id = Prelude.id
(.) = (Prelude..)
instance Functor ((->) e) where
type Dom ((->) e) = (->)
type Cod ((->) e) = (->)
fmap = (.)
instance Functor (->) where
type Dom (->) = Y (->)
type Cod (->) = Nat (->) (->)
fmap (Y f) = Nat (. f)
instance (Category p, Op p ~ Y p) => Category (Y p) where
type Op (Y p) = p
type Ob (Y p) = Ob p
id = Y id
Y f . Y g = Y (g . f)
source (Y f) = target f
target (Y f) = source f
unop = Y
op = getY
instance (Category p, Op p ~ Y p) => Functor (Y p a) where
type Dom (Y p a) = Y p
type Cod (Y p a) = (->)
fmap = (.)
instance (Category p, Op p ~ Y p) => Functor (Y p) where
type Dom (Y p) = p
type Cod (Y p) = Nat (Y p) (->)
fmap f = Nat (. Y f)
--------------------------------------------------------------------------------
-- Type Constraints
--------------------------------------------------------------------------------
infixl 1 \\ -- comment required for cpp
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
newtype p :- q = Sub (p => Dict q)
instance Functor Dict where
type Dom Dict = (:-)
type Cod Dict = (->)
fmap p Dict = case p of
Sub q -> q
instance Category (:-) where
id = Sub Dict
f . g = Sub (Dict \\ f \\ g)
instance Functor ((:-) e) where
type Dom ((:-) e) = (:-)
type Cod ((:-) e) = (->)
fmap = (.)
instance Functor (:-) where
type Dom (:-) = Y (:-)
type Cod (:-) = Nat (:-) (->)
fmap (Y f) = Nat (. f)
--------------------------------------------------------------------------------
-- * Common Functors
--------------------------------------------------------------------------------
instance Functor ((,) e) where
type Dom ((,) e) = (->)
type Cod ((,) e) = (->)
fmap f ~(a,b) = (a, f b)
instance Functor (Either e) where
type Dom (Either e) = (->)
type Cod (Either e) = (->)
fmap _ (Left a) = Left a
fmap f (Right b) = Right (f b)
instance Functor [] where
type Dom [] = (->)
type Cod [] = (->)
fmap = Prelude.fmap
instance Functor Prelude.Maybe where
type Dom Maybe = (->)
type Cod Maybe = (->)
fmap = Prelude.fmap
instance Functor IO where
type Dom IO = (->)
type Cod IO = (->)
fmap = Prelude.fmap
instance Functor (,) where
type Dom (,) = (->)
type Cod (,) = Nat (->) (->)
fmap f = Nat (\(a,b) -> (f a, b))
instance Functor Either where
type Dom Either = (->)
type Cod Either = Nat (->) (->)
fmap f0 = Nat (go f0) where
go :: (a -> b) -> Either a c -> Either b c
go f (Left a) = Left (f a)
go _ (Right b) = Right b
--------------------------------------------------------------------------------
-- * Groupoids
--------------------------------------------------------------------------------
class Category p => Groupoid p where
sym :: p a b -> p b a
instance (Category p, Groupoid q) => Groupoid (Nat p q) where
sym f@Nat{} = Nat (sym (runNat f))
--------------------------------------------------------------------------------
-- * Type Equality
--------------------------------------------------------------------------------
instance Category (:~:) where
type Op (:~:) = (:~:)
id = Refl
(.) = Prelude.flip Equality.trans
op = sym
unop = sym
instance Functor (:~:) where
type Dom (:~:) = (:~:)
type Cod (:~:) = Nat (:~:) (->)
fmap f = Nat (. Equality.sym f)
instance Functor ((:~:) e) where
type Dom ((:~:) e) = (:~:)
type Cod ((:~:) e) = (->)
fmap = (.)
instance Groupoid (:~:) where
sym = Equality.sym
--------------------------------------------------------------------------------
-- * Type Coercions
--------------------------------------------------------------------------------
instance Category Coercion where
type Op Coercion = Coercion
id = Coercion
(.) = Prelude.flip Coercion.trans
op = sym
unop = sym
instance Functor Coercion where
type Dom Coercion = Coercion
type Cod Coercion = Nat Coercion (->)
fmap f = Nat (. Coercion.sym f)
instance Functor (Coercion e) where
type Dom (Coercion e) = Coercion
type Cod (Coercion e) = (->)
fmap = (.)
instance Groupoid Coercion where
sym = Coercion.sym
@ttuegel
Copy link

ttuegel commented Mar 1, 2016

Concerning these definitions for source and target,

source :: p a b -> Dict (Ob p a)
target :: p a b -> Dict (Ob p b)

I considered this approach in my own work to allow "enriched" arrows which carry around their own dictionaries; this obviates the need for Ob p constraints on (.). I abandoned this after I convinced myself that a programmer could subvert the guarantees of the type system by calling source undefined, causing a run-time error. Was I concerned for nothing, or is there an issue here?

Copy link

ghost commented Mar 30, 2016

I don't understand the type of fmap in class Functor ...: surely it should be fmap :: Dom f a b -> Cod f (f a) (f b) rather than fmap :: p a b -> q (f a) (f b)?

Edit: sorry, I've just seen you say this in a video. Never mind...

@Icelandjack
Copy link

Yeah fmap should be

fmap :: Dom f a b -> Cod f (f a) (f b)

also

-- sym f@Nat{} = Nat (sym (runNat f))
sym (Nat f) = Nat (sym f)

Copy link

ghost commented Jun 26, 2016

I loaded this (with the type of fmap changed as mentioned above) into ghci and typed ":t fmap". It doesn't seem to terminate: 100 iterations of the constraints solver is not enough. Should it terminate?

@Icelandjack
Copy link

Icelandjack commented Oct 4, 2017

All of the Functor instances (except Functor Dict?) can be derived

@xsoufiane
Copy link

xsoufiane commented Aug 8, 2022

I had some trouble implementing category laws in quickcheck because of the Eq instance for functions, so I had the idea to add another function to the category class ap :: p a b -> a -> b to be able to apply the morphism and also be able to put Eq b. but b is not of kind Type so :(

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment