Skip to content

Instantly share code, notes, and snippets.

@danbornside

danbornside/Catty.hs

Last active March 28, 2018 03:26
Show Gist options
  • Save danbornside/f698d4f911a248949a488d1dc12511a2 to your computer and use it in GitHub Desktop.
Save danbornside/f698d4f911a248949a488d1dc12511a2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Catty.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
import Prelude (undefined)
class Category (hom :: k -> k -> *) where
id :: hom x x
(.) :: hom y z -> hom x y -> hom x z
newtype Op p a b = Op { unOp :: p b a }
data Trivial a b = Trivial
instance Category (->) where
id x = x
f . g = \x -> f (g x)
instance Category hom => Category (Op hom) where
id = Op id
Op x . Op y = Op (y . x)
instance Category Trivial where
id = Trivial
_ . _ = Trivial
class (Category c, Category d) => Functor c d (f :: k -> j) | f -> c, f -> d where
fmap :: c a b -> d (f a) (f b)
instance Functor (->) (->) ((->) r) where
fmap f g x = f (g x)
-- data Compose (c :: x -> x -> *) (d :: z -> z -> *) (c2d :: y -> y -> *) (f :: y -> z) (g :: x -> y) a b where
-- Compose :: (c a b -> d (f (g a)) (f (g b))) -> Compose c d c2d f g a b
-- instance (Functor c2d c f, Functor d c2d g) => Functor d c (Compose c d c2d f g u) where
-- fmap p = _f
-- where
-- fmapF = fmap @ c2d @ c @ f
-- fmapG = fmap @ d @ c2d @ g
-- fmapFG x = fmapF (fmapG x)
-- data Proj = Fst | Snd
--
-- data family Pair0 a b Proj
--
-- data Pair c d x y
-- = Pair :: c x y -> d x' y' -> Pair c d (Pair0 x x') (Pair0 y y')
newtype Nat (d :: j -> j -> *) (c :: k -> k -> *) (f :: j -> k) (g :: j -> k)
= Nat { nu :: forall a. c (f a) (g a) }
instance Category c => Category (Nat d c) where
id = Nat id
Nat f . Nat g = Nat (f . g)
newtype Leibniz c a b = Leibniz { cast :: forall f. c (f a) (f b) }
liftEq :: Category c => Leibniz (->) a b -> c a b
liftEq (Leibniz x) = x id
--liftEq' :: Category c => Leibniz (->) a b -> Leibniz c a b
-- liftEq' (Leibniz x) = Leibniz (_conj (x _conj' ))
-- invLeibniz :: Leibniz (->) a b -> Leibniz (->) b a
-- invLeibniz = from . liftEq
instance Category c => Category (Leibniz c) where
id = Leibniz id
Leibniz p . Leibniz q = Leibniz (p . q)
data I a = I { getI:: a }
data K x a = K { getK:: x }
data (:*:) f g a = (:*:) { getFst :: f a, getSnd :: g a}
data (:+:) f g a = Inl (f a)
| Inr (g a)
(*) f g (a :*: b) = f a :*: g b
f + g = \case
Inl as -> Inl (f as)
Inr bs -> Inr (g bs)
instance Functor (->) (->) I where
fmap f = I . f . getI
instance Functor (->) (->) (K x) where
fmap _ = K . id . getK
instance (Functor (->) (->) f, Functor (->) (->) g) => Functor (->) (->) (f :*: g) where
fmap f = fmap f * fmap f
instance (Functor (->) (->) f, Functor (->) (->) g) => Functor (->) (->) (f :+: g) where
fmap f = fmap f + fmap f
fmapCompose :: (Functor y z f, Functor x y g) => x a b -> z (f (g a)) (f (g b))
fmapCompose f = fmap (fmap f)
data (:**:) p q a b = (:**:) { getFst2 :: p a b, getSnd2 :: q a b}
instance (Category c, Category d) => Category (c :**: d) where
id = id :**: id
(p :**: q) . (p' :**: q') = (p . p') :**: (q . q')
-- | TASeq would be "better" but i don't have okasaki lying around...
data TAList p a b where
TANil :: TAList p a a
TACons :: p a b -> TAList p b c -> TAList p a c
-- | TAList is the free category!
instance Category (TAList p) where
id = TANil
(.) :: TAList p b c -> TAList p a b -> TAList p a c
q . TANil = q
q . (TACons p ps) = TACons p (q . ps)
foldCat :: (Functor c d f) => TAList c a b -> d (f a) (f b)
foldCat TANil = id
foldCat (TACons p qs) = foldCat qs . fmap p
catConcat :: Category c => TAList c a b -> c a b
catConcat TANil = id
catConcat (TACons p qs) = catConcat qs . p
-- instance (Functor y z f, Functor x y g) => Functor x z (Compose y f g) where
-- fmap = fmap . fmap
type Maybe = K () :+: I
-- class Category c => Groupoid c where
-- inv :: c a b -> c b a
-- instance Groupoid (Leibniz (->)) where
data Iso x y = Iso { to :: x -> y, from :: y -> x }
instance Category Iso where
id = Iso id id
(Iso b2c c2b) . (Iso a2b b2a) = Iso (b2c . a2b) (b2a . c2b)
--
-- instance Groupoid (Iso) where
class Category c => Monoidal (c :: k -> k -> *) where
type Unit c :: k
terminal :: c a (Unit c)
type Product c :: k -> k -> k
fst :: c (Product c x y) x
snd :: c (Product c x y) y
(***) :: c a b -> c x y -> c (Product c a x) (Product c b y)
idLeft :: c x (Product c (Unit c) x)
idRight :: c x (Product c x (Unit c))
assocLeft :: c (Product c (Product c x y) z) (Product c x (Product c y z))
assocRight :: c (Product c x (Product c y z)) (Product c (Product c x y) z)
instance Monoidal (->) where
type Unit (->) = ()
type Product (->) = (,)
fst (x, _) = x
snd (_, y) = y
f *** g = \(x, y) -> (f x, g y)
terminal _ = ()
idLeft x = ((), x)
idRight x = (x, ())
assocLeft ((x, y), z) = (x, (y, z))
assocRight (x, (y, z)) = ((x, y), z)
{-
- x :: Nat c F G === forall a. c (F a) (G a)
- y :: Nat c G H === forall a. c (G a) (H a)
- y . x :: Nat c F H === forall a. c (F a) (H a)
- id :: Nat c f f === forall a. c (f a) (f a)
-
-
-
- -}
type family KK (c :: k -> k -> *) (a :: j) :: k
type instance KK c a = Unit c
-- I think we aught to have something like:
-- instance CCC c => CCC (Nat c)
-- but i think we need all of the polynomial functors first.
-- instance Monoidal c => Monoidal (Nat d c) where
-- type Unit (Nat d c) = KK c
-- type Unit (Nat c) = Unit
--type Unit = c Unit
-- HOM f g :: forall a. c (f a) (g a)
-- HOM (f * f') (g * g') :: forall a.
-- HOM
class Monoidal hom => CCC hom where
type Hom hom :: k -> k -> k
curry :: hom (Product hom x y) z -> hom x (Hom hom y z)
uncurry :: hom x (Hom hom y z) -> hom (Product hom x y) z
instance CCC (->) where
type Hom (->) = (->)
curry f = \x y -> f (x, y)
uncurry f = \(x, y) -> f x y
--data I' c u a = I' { getI' :: c u a }
--instance Category c => Category (I' c) where
-- id = I' id
-- I' f . I' g = I' (f . g)
--
--instance Category c => Functor (I' c) (I' c) (I' c u) where
-- fmap = _fmap
data K' c u x a = K' (c u x)
-- instance Category c => Functor c c (K' c u x) where
-- fmap c = liftEq (Leibniz _x)
main = undefined
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment