Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Last active Oct 10, 2020
Embed
What would you like to do?
Functor
{-
Every functor is a function mapping categories.
I want to specify them all in one place,
instance Functor (->) where
type Arr (->) = (<–) :- (->) :- End (->)
without having to specified partial applications of it
-- instance Functor (a ->) where
-- type Arr (a ->) = (->) :- End (->)
I also want to be able to have "obvious" arrow inferred
instance Functor (,,,) where
type Arr (,,,) = (->) :- (->) :- (->) :- (->) :- End (->)
=
type Arr (,,,) = (->) :- (->) :- (->) :- (->) :- DefCats @Type
=
type Arr (,,,) = (->) :- (->) :- (->) :- DefCats @(Type->Type)
=
type Arr (,,,) = (->) :- (->) :- DefCats @(Type->Type->Type)
=
type Arr (,,,) = (->) :- DefCats @(Type->Type->Type->Type)
=
type Arr (,,,) = DefCats @(Type->Type->Type->Type->Type)
So might as well add it
class Functor (f :: s -> t) where
type Arr (f :: s -> t) :: Cats (s -> t)
type Arr (_ :: s -> t) = DefCats @(s -> t)
-}
import Data.Kind
import Data.Function hiding (id, (.))
import GHC.Exts (Any)
import Prelude hiding (Functor(fmap), map, id, (.))
import Control.Category
import Data.Coerce
type Cat :: Type -> Type
type Cat ob = ob -> ob -> Type
type Cats :: Type -> Type
data Cats obs where
End
:: Cat ob
-> Cats ob
(:-)
:: Cat ob
-> Cats obs
-> Cats (ob->obs)
infixr 5
:-
type
Tail :: Cats (ob -> obs) -> Cats obs
type family
Tail cats where
Tail (_ :- cats) = cats
type
Head :: Cats (ob -> obs) -> Cat ob
type family
Head cats where
Head (cat :- cats) = cat
type Uncons :: Cat ob -> Cats obs -> Cats (ob -> obs) -> Constraint
class (head ~ Head as, tail ~ Tail as) => (head `Uncons` tail) as
instance (head ~ Head as, tail ~ Tail as) => (head `Uncons` tail) as
type
(-->) :: forall ob. Cat ob
type family
(-->)
type instance
(-->) @Type = (->)
type
DefCats :: forall obs. Cats obs
type family
DefCats where
DefCats @(ob->obs) = (-->) @ob :- DefCats @obs
DefCats @ob = End ((-->) @ob)
type (~>) :: forall k. Cat (k -> Type)
type f ~> f' = (forall x. f x -> f' x)
type (~~>) :: forall k j. Cat (k -> j -> Type)
type f ~~> f' = (forall x. f x ~> f' x)
-- type
-- Ans :: Cats ~> Cat
-- data family
-- Ans cats
-- newtype instance
-- Ans (End cat) a1 a2 where
-- Yes :: cat a1 a2 -> Ans (End cat) a1 a2
-- newtype instance
-- Ans (cat :- cats) f1 f2 where
-- No :: (forall a1 a2. cat a1 a2 -> Ans cats (f1 a1) (f2 a2))
-- -> Ans (cat :- cats) f1 f2
type Ans :: Cats ~> Cat
data Ans cats a1 a2 where
Yes :: cat a1 a2
-> Ans (End cat) a1 a2
No :: (forall a1 a2. cat a1 a2 -> Ans cats (f1 a1) (f2 a2))
-> Ans (cat :- cats) f1 f2
-- Arr f :: Cats (s -> t)
type
AllCategories :: Cats obs -> Constraint
type family
AllCategories as where
AllCategories (End cat) = Category cat
AllCategories (cat:-cats) = (Category cat, AllCategories cats)
type Map :: (s -> t) -> Type
type Map f = Ans (Arr f) f f
type Functor :: (s -> t) -> Constraint
class AllCategories (Arr f) => Functor (f :: s -> t) where
type Arr (f :: s -> t) :: Cats (s -> t)
fmap :: Map f
instance Functor @Type @Type [] where
type Arr [] = (->) :- End (->)
fmap :: Map []
fmap = map1 \f -> fix \map'f -> \case
[] -> []
a:as -> f a:map'f as
-- type Eta :: Cats (ob -> obs) -> Constraint
-- class (Head cats :- Tail cats) ~ cats => Eta cats
-- instance (Head cats :- Tail cats) ~ cats => Eta cats
-- TODO: fix constraints
instance (Category (Head (Arr f)), Functor f, AllCategories (Tail (Arr f))) => Functor (f a) where
type Arr (f a) = Tail (Arr f)
fmap :: Map (f a)
fmap | No f <- fmap @_ @_ @f = f id
-- map1 :: (forall a1 a2. src a1 a2 -> tgt (f a1) (f a2)) -> Ans (src :- tgt) f f
-- map1 f = No (Yes f)
-- ∀a1 a2. acat a1 a2 -> (∀b1 b2. bcat b1 b2 -> ccat (f a1 b1) (f a2 b2))
-- ∀a1 a2. acat a1 a2 -> (∀b1 b2. bcat b1 b2 -> ccat (f a1 b1) (f a2 b2))
map0 :: cat ~~> Ans (End cat)
map0 = Yes
map1 :: (forall a1 a2. src a1 a2 -> tgt (f1 a1) (f2 a2)) -> Ans (src:-End tgt) f1 f2
map1 body = No \f -> Yes do body f
map1op :: Ans (src:-End tgt) f1 f2 -> (forall a1 a2. src a1 a2 -> tgt (f1 a1) (f2 a2))
map1op (No body) (body -> Yes body') = body'
pattern Yes1 :: (forall a1 a2. src a1 a2 -> tgt (f1 a1) (f2 a2)) -> Ans (src:-End tgt) f1 f2
pattern Yes1 f <- (map1op -> f)
where Yes1 = map1
map2 :: (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> tgt (f1 a1 b1) (f2 a2 b2))
-> Ans (src:-src':-End tgt) f1 f2
map2 body = No \f -> No \f' -> Yes do body f f'
map2op :: Ans (src:-src':-End tgt) f1 f2
-> (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> tgt (f1 a1 b1) (f2 a2 b2))
map2op (No body) (body -> No body') (body' -> Yes body'') = body''
pattern Yes2 :: (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> tgt (f1 a1 b1) (f2 a2 b2))
-> Ans (src:-src':-End tgt) f1 f2
pattern Yes2 f <- (map2op -> f)
where Yes2 = map2
map3 :: (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> forall c1 c2. src'' c1 c2 -> tgt (f1 a1 b1 c1) (f2 a2 b2 c2))
-> Ans (src:-src':-src'':-End tgt) f1 f2
map3 body = No \f -> No \f' -> No \f'' -> Yes do body f f' f''
map3op :: Ans (src:-src':-src'':-End tgt) f1 f2
-> (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> forall c1 c2. src'' c1 c2 -> tgt (f1 a1 b1 c1) (f2 a2 b2 c2))
map3op (No body) (body -> No body') (body' -> No body'') (body'' -> Yes body''') = body'''
pattern Yes3 :: (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> forall c1 c2. src'' c1 c2 -> tgt (f1 a1 b1 c1) (f2 a2 b2 c2))
-> Ans (src:-src':-src'':-End tgt) f1 f2
pattern Yes3 f <- (map3op -> f)
where Yes3 = map3
map4 :: (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> forall c1 c2. src'' c1 c2 -> forall d1 d2. src''' d1 d2 -> tgt (f1 a1 b1 c1 d1) (f2 a2 b2 c2 d2))
-> Ans (src:-src':-src'':-src''':-End tgt) f1 f2
map4 body = No \f -> No \f' -> No \f'' -> No \f''' -> Yes do body f f' f'' f'''
map4op :: Ans (src:-src':-src'':-src''':-End tgt) f1 f2
-> (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> forall c1 c2. src'' c1 c2 -> forall d1 d2. src''' d1 d2 -> tgt (f1 a1 b1 c1 d1) (f2 a2 b2 c2 d2))
map4op (No body) (body -> No body') (body' -> No body'') (body'' -> No body''') (body''' -> Yes body'''') = body''''
pattern Yes4 :: (forall a1 a2. src a1 a2 -> forall b1 b2. src' b1 b2 -> forall c1 c2. src'' c1 c2 -> forall d1 d2. src''' d1 d2 -> tgt (f1 a1 b1 c1 d1) (f2 a2 b2 c2 d2))
-> Ans (src:-src':-src'':-src''':-End tgt) f1 f2
pattern Yes4 f <- (map4op -> f)
where Yes4 = map4
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 10, 2020

instance Functor (,,,) where
 fmap :: Map (,,,)
 fmap = Yes4 \one two three four (a, b, c, d) -> (one a, two b, three c, four d)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment