Last active
October 10, 2020 16:06
-
-
Save Icelandjack/ec1d3944551f1b53b6eb17b51824a396 to your computer and use it in GitHub Desktop.
Functor
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- | |
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 |
Author
Icelandjack
commented
Oct 10, 2020
•
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment