Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Functors

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
@Icelandjack
Copy link
Author

Icelandjack commented Dec 12, 2017

http://www.informatik.uni-marburg.de/%7Erendel/unparse/rendel10invertible.pdf

class IsoFunctor f where
  (<$>) :: Iso a b -> (f a -> f b)

class IsoApplicative f where
  (<*>) :: f (Iso a b) -> (f a -> f b)

@Icelandjack
Copy link
Author

Icelandjack commented Dec 13, 2017

newtype Cont r a = Cont ((a => r) -> r)

class Bind f where
  ret :: Dict ~> f

instance Bind (Cont r) where
  re :: Dict ~> Cont r
  re Dict = Cont id

v

http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight.pdf

class Bind r where
  var :: Var r a -> r a

  lam :: (Var r a -> r b) -> r (a -> b)

@Icelandjack
Copy link
Author

Icelandjack commented Dec 25, 2017

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?

@Icelandjack
Copy link
Author

Icelandjack commented Dec 27, 2017

data WitnessEq :: k -> k -> Type where
  WitnessEq :: ((a :== b) ~ True) => WitnessEq a b

@Icelandjack
Copy link
Author

Icelandjack commented Feb 17, 2018

http://homepages.inf.ed.ac.uk/als/ScottInScotland/ghani.pdf

Predicates: The category of predicates has

  • Objects: Predicates P :: X -> Type
  • Arrows: (X, P) -> (X', P') are pairs f :: X -> X' and f' :: forall xx. P xx -> P' (f xx)
data Predic :: Cat k' -> Cat (k -> k') where
  Predic 
    :: Sing (fun :: k --> k)
    -> (forall xx. p xx `cat` p' (fun @@ xx))
    -> Predic cat p p'

instance Category cat => Category (Predic cat) where
  id :: Predic cat p p
  id = Predic (singFun1 @IdSym0 sId) id

  (.) :: forall b c a. Predic cat b c -> Predic cat a b -> Predic cat a c
  Predic (s'::Sing fun) x' . Predic (s::Sing fun') x = 
    Predic (singFun1 @(fun :.$$$ fun') (s' %:. s)) (x' . x)

@Icelandjack
Copy link
Author

Icelandjack commented Feb 26, 2018

http://cs.ioc.ee/~tarmo/tsem11/jeltsch0902-slides.pdf

class SafeFunctor f where
  safeMap :: (forall tt. At tt a -> At tt a') -> (At t (f a) -> At t (f a'))

@Icelandjack
Copy link
Author

Icelandjack commented Feb 28, 2018

[40:22] https://www.youtube.com/watch?v=Bxcz23GOJqc

-- functor from Monads to Monads
class MonadTrans trans => Transformer trans where
  hoist :: (Monad m, Monad m') => (m ~> m') -> (trans m ~> trans m')

@Icelandjack
Copy link
Author

Icelandjack commented Mar 21, 2018

Semantic function (http://drops.dagstuhl.de/opus/volltexte/2018/8479/pdf/LIPIcs-TYPES-2015-9.pdf) for circuits

instance Functor (Vec Bool) where
  type Dom (Vec Bool) = C
  type Dom (Vec Bool) = (->)

  map :: C i o -> (Vec Bool i -> Vec Bool o)

@Icelandjack
Copy link
Author

Icelandjack commented Apr 1, 2018

@Icelandjack
Copy link
Author

Icelandjack commented Apr 8, 2018

https://github.com/pigworker/EGTBS/blob/master/EGTBS.pdf

weakening :: (iz <= jz) -> (Lam iz -> Lam jz)

@Icelandjack
Copy link
Author

Icelandjack commented May 14, 2018

https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf

map :: (v ~> v') -> (IHashMap k v -> IHashMap k v')

@Icelandjack
Copy link
Author

Icelandjack commented Jun 5, 2018

https://pdfs.semanticscholar.org/presentation/1388/78774b81cb5e2c6b96d71c0dc39272ccd608.pdf

Functorial semantics

fmap :: Circuit i o -> (Vec Bool i -> Vec Bool o)

-- unfmap? (fully faithful functor to opposite cat)
Plug :: (Fin o -> Fin i) -> Circuit i o

@Icelandjack
Copy link
Author

Icelandjack commented Jun 11, 2018

http://hackage.haskell.org/package/backprop-0.2.4.0/docs/Numeric-Backprop.html

evalBP :: (forall s. Reifies s W. BVar s a -> BVar s b) -> (a -> b)

unmap without an fmap.. idk

@Icelandjack
Copy link
Author

Icelandjack commented Jun 11, 2018

Oh also

onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a 
onIxPred f = \case 
  IZ -> IZ
  IS x -> IS $ f x

@Icelandjack
Copy link
Author

Icelandjack commented Jun 26, 2018

http://www2.sf.ecei.tohoku.ac.jp/~kztk/papers/kztk_jfp_am_2018.pdf

class LFunctor f where
  lift :: Lens a b -> (f a -> f b)

class LFunctor f => LMonoidal f where
  unit  :: f ()
  (<*>) :: f a -> f b -> f (a, b)

@Icelandjack
Copy link
Author

Icelandjack commented Jun 26, 2018

{- |
The lifting function. Note that it forms a functor from the
category of lenses to the category of sets and functions.

'unlift' is a left-inverse of this function.

prop> unlift (lift x) = x
-}
{-
Notice that 'lift' is not a surjection. That is,
there is a function such that @lift (unlift f) /= f@.
However such a function cannot be constructed with `lift`.
-}
lift :: L.Lens' a b -> (forall s. L s a -> L s b)
lift l = liftI (fromLens l)

liftI :: LensI a b -> (forall s. L s a -> L s b)
liftI h = \(L x) -> L (h <<< x)

https://bitbucket.org/kztk/app-lens/src/83376a9b25bc483c65776db48b33593601d274bd/Control/LensFunction/Core.hs?at=master&fileviewer=file-view-default

@Icelandjack
Copy link
Author

Icelandjack commented Jun 30, 2018

Implementation of https://forum.azimuthproject.org/discussion/2213/lecture-38-chapter-3-databases/p1

type Grph node = node -> node -> Type

data Node = Employee | Department | Str

data Work :: Grph Node where
  Manager   :: Work Employee   Employee
  WorksIn   :: Work Employee   Department
  Secretary :: Work Department Employee 
  FirstName :: Work Employee   Str
  DepName   :: Work Department Str

data Empl = Empl
  { name    :: String
  , manager :: Empl
  , dep     :: Dep
  }

data Dep = Dep
  { depName   :: String
  , secretary :: Empl
  }

type family
  El (node :: Node) = (res :: Type) | res -> node where
  El Employee   = Empl
  El Department = Dep
  El Str        = String

varp :: Work a b -> (El a -> El b)
varp = \case
  Manager -> 
    manager

  WorksIn -> 
    dep

  Secretary -> 
    secretary

  FirstName -> 
    name

  DepName -> 
    depName
-- The free category
data Free :: Cat ob -> Cat ob where
  Base :: Free cat a a

  (:·) :: cat a b 
       -> Free cat b c
       -> Free cat a c
infixr 

varp2 :: Free Work a b -> (El a -> El b)
varp2 = \case
  Base -> 
    id

  w  ws -> 
    varp2 ws . varp w 

@Icelandjack
Copy link
Author

Icelandjack commented Jul 22, 2018

@Icelandjack
Copy link
Author

Icelandjack commented Aug 27, 2018

dropEnv :: Env m ys -> SubList xs ys -> Env m xs
dropEnv Empty SubNil = Empty
dropEnv (v :> vs) (Keep rest) = v :> dropEnv vs rest
dropEnv (_ :> vs) (Drop rest) = dropEnv vs rest

https://github.com/goldfirere/effects/blob/master/Effects.hs

@Icelandjack
Copy link
Author

Icelandjack commented Sep 5, 2018

https://www.reddit.com/r/haskell/comments/9cvtc0/new_blog_post_compositional_zooming_for_statet/

zoom :: Lens' st st' -> State st' a -> State st  a
zoom = id

instance Functor State where
  type Dom State = Y ReifiedLens' -- yeahyeah
  type Cod State = Nat (->) (->)

  fmap :: Y ReifiedLens' st st' -> (State st ~> State st')
  fmap (Y (ReifiedLens lens)) = Nat lens -- something

@Icelandjack
Copy link
Author

Icelandjack commented Oct 17, 2018

@Icelandjack
Copy link
Author

Icelandjack commented Oct 20, 2018

data
  Fin  :: N -> Type where
  FinO :: Fin (S n)
  FinS :: Fin n -> Fin (S n)

data (<=) :: Cat N where
  LTEO ::   (O <= m)
  LTES ::   (n <= m)
       -> (S n <= S m)

trust :: Fin O `Coercion` Fin n'
trust = unsafeCoerce (Coercion :: forall gensym. Coercion gensym gensym)

instance Functor Fin where
  type Dom Fin = (<=)
  type Cod Fin = Coercion

  fmap ::      (n <= n')
     -- _________________________
     -> (Fin n `Coercion` Fin n')
  fmap = \case
    LTEO ->
      trust

    LTES lte
      | Coercion :: Fin   (pred_n) `Coercion` Fin   (pred_n') <- fmap lte
     -> Coercion :: Fin (S pred_n) `Coercion` Fin (S pred_n')

@Icelandjack
Copy link
Author

Icelandjack commented Oct 20, 2018

https://hott.github.io/book/nightly/hott-online-1186-gee8923a.pdf

functions respect equality

ap @f :: (a :~: a') -> (f a :~: f a')

@Icelandjack
Copy link
Author

Icelandjack commented Oct 25, 2018

data Sublist (super :: [k]) (sub :: [k]) where
  SublistNil :: Sublist '[]
  SublistSuper :: Proxy r -> Sublist super sub -> Sublist (r ': super) sub 
  SublistBoth :: Proxy r -> Sublist super sub -> Sublist (r ': super) (r ': sub)

projectRec :: Sublist super sub -> Rec f super -> Rec f sub
projectRec s r = case s of SublistNil -> RNil SublistBoth n snext -> case r of rhead :& rtail -> rhead :& projectRec snext rtail SublistSuper n snext -> case r of rhead :& rtail -> projectRec snext rtail

http://hackage.haskell.org/package/vinyl-0.10.0/docs/Data-Vinyl-Class-Method.html#t:PayloadType

@Icelandjack
Copy link
Author

Icelandjack commented Dec 12, 2018

https://github.com/sjoerdvisscher/data-category/blob/master/Data/Category/Simplex.hs

a `FunctorOf Fin Simplex (->)

data Forget = Forget
-- | Turn @Simplex x y@ arrows into @Fin x -> Fin y@ functions.
instance Functor Forget where
  type Dom Forget = Simplex
  type Cod Forget = (->)
  type Forget :% n = Fin n
  Forget % Z   = \x -> x
  Forget % Y f = \x -> Fs ((Forget % f) x)
  Forget % X f = \x -> case x of
    Fz -> Fz
    Fs n -> (Forget % f) n

@Icelandjack
Copy link
Author

Icelandjack commented Jan 19, 2019

https://www.reddit.com/r/haskell/comments/2q5bdb/monads_need_not_be_endofunctors_we_introduce_a/

data Fin :: Nat -> * where  -- each Fin n is finite, of size n
  Fz :: Fin (Suc n)
  Fs :: Fin n -> Fin (Suc n)

data Term :: Nat -> * where
  Var :: Fin n -> Term n
  (:$) :: Term n -> Term n -> Term n
  Lam :: Term (Suc n) -> Term n

instance Functor_ 'id where
  type Dom 'id = FinCat
  type Cod 'id = TermCat

  fmap_ :: n `FinCat` n'
        -> n `TermCat` n'
  fmap_ = ... 

@Icelandjack
Copy link
Author

Icelandjack commented May 15, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment