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 xsdata 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 :$ expinfixr :->
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 :$ expE 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 0aaah 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 = Reflinstance 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 = (=<<) . runKleisliWorks 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
FunctorOf (~>) (->): https://github.com/kwf/StrictCheck/blob/master/StrictCheck/src/Test/StrictCheck/Shaped.hs