Skip to content

Instantly share code, notes, and snippets.

@rampion
Last active August 29, 2015 14:05
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save rampion/aa9e8a7a61853c3042e7 to your computer and use it in GitHub Desktop.
Save rampion/aa9e8a7a61853c3042e7 to your computer and use it in GitHub Desktop.
Solution for [Bicategories in Haskell](http://stackoverflow.com/questions/25210743/bicategories-in-haskell) on StackOverflow
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module SO25210743 where
import Prelude hiding (fmap, Functor, id, (.))
import GHC.Prim
class Category (c :: * -> * -> *) where
id :: c x x
(.) ::c y z -> c x y -> c x z
class Category c => Arr c where
arr :: (x -> y) -> c x y -- stolen from Control.Arrow.Arrow
class Functor c d f where
fmap :: c x y -> d (f x) (f y)
newtype Compose g f t = Compose { unCompose :: g (f t) }
-- Compose :: g (f t) -> Compose g f t
-- unCompose :: Compose g f t -> g (f t)
instance (Functor c d f, Functor d e g, Arr e) => Functor c e (Compose g f) where
-- c :: c x y
-- fmap_cdf c :: d (f x) (f y)
-- fmap_deg (fmap_cdf c) :: e (g (f x)) (g (f y))
-- arr Compose :: e (g (f y)) (Compose g f y)
-- arr unCompose :: e (Compose g f x) (g (f x))
-- arr Compose . fmap_deg (fmap_cdf c) . arr unCompose
-- :: e (Compose g f x) (Compose g f y)
fmap c = arr Compose . fmap_deg (fmap_cdf c) . arr unCompose
where fmap_cdf :: forall x y. c x y -> d (f x) (f y)
fmap_cdf = fmap
fmap_deg :: forall x y. d x y -> e (g x) (g y)
fmap_deg = fmap
newtype NT c f g = NT { unNT :: forall x. c (f x) (g x) }
class Bicategory (bicat :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) comp where
id1 :: Category c => bicat c f f
(.|) :: Category c => bicat c g h -> bicat c f g -> bicat c f h
(.-) :: (Functor c d g, Arr d) => bicat d g g' -> bicat c f f' -> bicat d (comp g f) (comp g' f')
instance Bicategory NT Compose where
id1 = NT id
NT n .| NT m = NT (n . m)
-- m :: c (f x) (f' x)
-- fmap m :: d (g (f x)) (g (f' x))
-- n :: d (g (f' x)) (g' (f' x))
-- n . fmap m :: d (g (f x)) (g' (f' x))
-- arr Compose :: d (g' (f' x)) (Compose g' f' x)
-- arr unCompose :: d (Compose g f x) (g (f x))
-- arr Compose . n . fmap m . arr unCompose
-- :: d (Compose g f x) (Compose g' f' x)
NT n .- NT m = NT $ arr Compose . n . fmap m . arr unCompose
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment