type Cat k = k -> k -> Type
data Sublist :: Cat [a] where
Stop :: Sublist '[] '[]
Drop :: Sublist xs ys -> Sublist (x:xs) ys
Keep :: Sublist xs ys -> Sublist (x:xs) (x:ys)
data HList :: [Type] -> Type where
HNil :: HList '[]
HCons :: a -> HList as -> HList (a:as)
deriving instance ShowAll xs => Show (HList xs)
type family
ShowAll as :: Constraint where
ShowAll '[] = ()
ShowAll (x:xs) = (Show x, ShowAll xs)
hfmap :: (Sublist xs xs') -> (HList xs -> HList xs')
hfmap Stop HNil = HNil
hfmap (Drop a) (HCons x xs) = hfmap a xs
hfmap (Keep a) (HCons x xs) = HCons x (hfmap a xs)
dropEveryOther :: HList '[a,b,c,d] -> HList '[b,d]
dropEveryOther = hfmap (Drop $ Keep $ Drop $ Keep $ Stop)
xs :: HList '[Int, Bool, Float, ()]
xs = HCons 10
$ HCons False
$ HCons pi
$ HCons ()
$ HNil
ys :: HList '[Bool, ()]
ys = dropEveryOther xs
data Funs :: Cat Type -> Cat [Type] where
FNil :: Funs cat '[] '[]
FCons :: cat a b
-> Funs cat as bs
-> Funs cat (a:as) (b:bs)
Is a category thusly
class Gen xs where
mkId :: Category cat => Funs cat xs xs
instance Gen '[] where
mkId :: Category cat => Funs cat '[] '[]
mkId = FNil
instance Gen as => Gen (a ': as) where
mkId :: Category cat => Funs cat (a ': as) (a ': as)
mkId = FCons id mkId
id_ :: (Category cat, Gen xs) => (Funs cat) xs xs
id_ = mkId
comp :: Category cat => Funs cat ys zs -> Funs cat xs ys -> Funs cat xs zs
comp FNil FNil = FNil
comp (FCons f fs) (FCons g gs) = FCons (f . g) (comp fs gs)
and fmap
would be defined
instance Functor HList where
type Dom HList = Funs (->)
type Cod HList = (->)
fmap :: Funs (->) as as' -> (HList as -> HList as')
fmap FNil HNil = HNil
fmap (FCons f fs) (HCons x xs) = HCons (f x) (fmap fs xs)
fmap (FCons show (FCons not FNil)) :: HList '[Char, Bool] -> HList '[String, Bool]
>>> fmap (FCons show (FCons not FNil)) (HCons 'a' (HCons False HNil))
HCons "'a'" (HCons True HNil)
Probably doesn't satisfy laws
data N = O | S N
data (>=) :: Cat N where
GeO :: O >= O
GeS :: n >= m -> S n >= S m
data Vect :: N -> Type -> Type where
VNil :: Vect O a
VCons :: a -> Vect n a -> Vect (S n) a
vectMap :: (n >= n') -> (Vect n a -> Vect n' a)
data (<=) :: Cat N where
LeO :: O <= m
LeS :: n <= m -> S n <= S m
finMap :: (n <= n') -> (Fin n -> Fin n')
finMap (LeS l) FO = FO
finMap (LeS l) (FS n) = FS (finMap l n)
Based on Richard's Glambda
-- SubArr :: [Type] -> Cat Type
type SubArr xs a a' = Exp (a:xs) a'
-- Exp xs : SubArr xs -> (->)
fmapSubArr :: SubArr xs a a' -> Exp xs a -> Exp xs a'
fmapSubArr = flip subst
-- aka (untested)
-- instance Functor (Exp xs) where
-- type Dom (Exp xs) = SubArr xs
-- type Cod (Exp xs) = (->)
idSub :: SubArr xs a a
idSub = Var EZ
compSub :: SubArr xs b c -> SubArr xs a b -> SubArr xs a c
compSub as bc = undefined
infixl :$
data E a where
I :: Int -> E Int
Add :: E (Int -> Int -> Int)
Lam_ :: Blind (E a -> E b) -> E (a -> b)
(:$) :: E (a -> b) -> (E a -> E b)
deriving instance Show (E a)
pattern Lam a = Lam_ (Blind a)
newtype EFun a b = EFun (E (a -> b))
instance C.Category EFun where
id = EFun (Lam id)
EFun f . EFun g = EFun $ Lam $ \a ->
f :$ (g :$ a)
eMap :: EFun a a' -> (E a -> E a')
eMap (EFun fn) exp = fn :$ exp
infixr :->
data T = INT | T :-> T
-- infixl :$
data E :: T -> * where
I :: Int -> E INT
Add :: E (INT :-> INT :-> INT)
Lam_ :: Blind (E a -> E b) -> E (a :-> b)
(:$) :: E (a :-> b) -> (E a -> E b)
deriving instance Show (E a)
-- pattern Lam :: (E a -> E b) -> E (a -> b)
pattern Lam a = Lam_ (Blind a)
newtype EFun a b = EFun (E (a :-> b))
instance C.Category EFun where
id = EFun (Lam id)
EFun f . EFun g = EFun $ Lam $ \a ->
f :$ (g :$ a)
eMap :: EFun a a' -> (E a -> E a')
eMap (EFun fn) exp = fn :$ exp
E
as a functor mapping (0 : Int)
to False
and { n : Int | n /= 0 }
to True
infixr :->
data T = INT | T :-> T | BOOL
data E :: T -> * where
I :: Int -> E INT
Eq :: E (INT :-> INT :-> BOOL)
Lam_ :: Blind (E a -> E b) -> E (a :-> b)
(:$) :: E (a :-> b) -> (E a -> E b)
deriving instance Show (E a)
data Int2Bool a b where
I2B :: Int2Bool INT BOOL
pattern T = Eq :$ I 0 :$ I 0
pattern F = Eq :$ I 1 :$ I 0
i2bMap :: Int2Bool a a' -> (E a -> E a')
i2bMap I2B ea =
Eq :$ ea :$ I 0
aaah but Int2Bool
doesn't even form a category, we can maybe adjoin an identity: it is basically the free category over Int2Bool
data Cat :: Cat k -> Cat k where
Nil :: Cat f a a
Cons :: f a b -> Cat f b c -> Cat f a c
type Int2Bool' = FreeCat Int2Bool
i2bMap :: FreeCat Int2Bool a a' -> (E a -> E a')
i2bMap Nil = id
i2bMap (Cons I2B Nil) = (Eq :$ I 0 :$)
Edward has talked about packing a Num a
dictionary within V2 a
:
data V2 :: Type -> Type where
V2 :: Num a => a -> a -> V2 a
fmapNum :: Num a' => (a -> a') -> (V2 a -> V2 a')
fmapNum f (V2 a b) = V2 (f a) (f b)
there is only a Num a'
constraint on the result type a'
. Why not on a
? Because our V2 a
packs (provides) proof that a
is a number, but (f :: a -> a')
can map to any unrelated type: we have no Earthly idea what it is: so we constrain the output Num a'
.
What we need is a richer domain for V2
to be a functor. We need an arrow type that knows that its output is a number:
type Cat k = k -> k -> Type
data NumArr :: Cat Type where
NA :: Num a' => (a -> a') -> NumArr a a'
and now our fmap
fits the bill:
instance Functor V2 where
type Dom V2 = NumArr
type Cod V2 = (->)
(<$>) :: NumArr a a' -> (V2 a -> V2 a')
NA f <$> V2 a b = V2 (f a) (f b)
we can then start parameterizing it by the unsaturated constraint.
This is essentially the Haskell Functor category? Since you can only be a Functor
if you are generative (maybe matchable), an unsaturated type family cannot be an instance of Functor
even though GHC "lies" that its kind is the same.
data Lst f a a' where
Lst :: (as ~ f xx, as' ~ f yy) => (as -> as') -> Lst f as as'
fmap :: Functor f => (a -> a') -> Lst f (_ a) (_ a')
fmap f = Lst (fmap f)
where the objects of a functor's codomain is restricted to the form f _
. I have an idea using injective type families (TypeFamilyDependencies
) once they fix that bug, but this only works for a single Functor
at a time?
type family
UnList as = res | res -> as where
UnList [a] = a
newtype UnListArr :: Cat Type where
UnListArr :: (UnList xs -> UnList xs') -> UnListArr (UnList xs) (UnList xs')
fmap :: (UnList xs -> UnList xs') -> (xs -> xs')
-- or this which fit 'Functor'
fmap :: UnListArr xs xs' -> (xs -> xs')
Then we can abstract out the underlying category
data Lst :: Cat k -> (k' -> k) -> Cat k where
Lst :: (as ~ f xx, as' ~ f yy) => cat as as' -> Lst cat f as as'
fmapLst :: Functor f => (a -> a') -> Lst (->) f (_ a) (_ a')
fmapLst f = Lst (fmap f)
So maybe we can end up writing
class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
type Dom f :: Cat i
type Cod f :: Cat j
fmap :: (Dom f) a a' -> Lst (Cod f) f (f a) (f a')
probably in no way useful, but it is interesting to get even closer to a categorical functor..
From reddit
instance Functor [] where
type Dom [] = Equal
type Cod [] = Equal
fmap :: a:~:a' -> [a]:~:[a']
fmap Refl = Refl
instance Functor [] where
type Dom [] = (->)
type Cod [] = MonoidMorphism
fmap :: (a -> a') -> MonoidMorphism [a] [a']
fmap f = MM (map f)
instance Functor [] where
type Dom [] = Kleisli []
type Cod [] = (->)
fmap :: Kleisli [] a a' -> ([a] -> [a'])
fmap = (=<<) . runKleisli
Works for any Monad m
newtype KleiMon m a = KleiMon (m a)
instance Monad m => Functor (KleiMon m) where
type Dom (KleiMon m) = Kleisli m
type Cod (KleiMon m) = (->)
fmap :: (Kleisli m) a a' -> (m a -> m a')
fmap = (=<<) . runKleisli
https://twitter.com/int_index/status/945312890470486017
Learning category theory in Haskell should not start with the Hask category! Start with categories where objects are at the term level. Look at the additional structure that types have (e.g. orderings) and functions that preserve this structure.
Here is an exercise for you: tell me why the 'Data.Char.ord' function is a functor. What is its source category, what is its target category, what structure does it preserve?