Icelandjack/Functors.markdown

## Functors.markdown

      
    Raw
  

              Functors.markdown
            
          
    HList : Sublist -> Hask

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
HList : Funs (->) -> (->)

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)
Vect : N -> (~>)

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)
Fin : N -> (->)

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)
Exp xs : SubArr xs -> (->)

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 
E : EFun -> (->)

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
(deep indexing) E : EFun -> (->)

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
(deep index) E : Int2Bool -> (->)

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 :$)
V2 : NumArr -> (->)

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.
f : (->) -> Lst f

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)
f : cat1 -> Lst cat2 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
[] : (->) -> MonoidMorphism

instance Functor [] where
  type Dom [] = (->)
  type Cod [] = MonoidMorphism
  
  fmap :: (a -> a') -> MonoidMorphism [a] [a']
  fmap f = MM (map f)
[] : Kleisli [] -> (->)

instance Functor [] where
  type Dom [] = Kleisli []
  type Cod [] = (->)
  
  fmap :: Kleisli [] a a' -> ([a] -> [a']) 
  fmap = (=<<) . runKleisli
M : Kleisli M -> (->)

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