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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented May 29, 2017

As in http://emorehouse.web.wesleyan.edu/research/notes/basic_category_theory.pdf

fmap :: ctx |- M : A -> [| ctx |] -> [| A |]

so something like

newtype ctx |- a = Ctx (Exp '[ctx] a)

newtype Interp :: TY -> Type where
  Interp :: INTERP a -> Interp a

type family
  INTERP (a :: Ty) :: Type where
  INTERP I         = Int
  INTERP B         = Bool
  INTERP (a :-> b) = INTERP a -> INTERP b

fmap :: Exp [] (a -> b) -> (Interp a -> Interp b)

instance Functor Interp where
  type Dom Interp = (|-)
  type Cod Interp = (->)
  
  fmap :: a |- a' -> (Interp a -> Interp a')

fmap :: ctx |- M : A -> [| ctx |] -> [| A |]
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented May 31, 2017

How is Elem a functor

data Elem :: [a] -> a -> * where
  EZ :: Elem (x ': xs) x
  ES :: Elem xs x -> Elem (y ': xs) x
fmap :: Sublist xs xs' -> Elem xs ~> Elem xs'

Any interesting functors for

data Ty = I | B | Ty :> Ty | P Ty Ty

data Exp :: [Ty] -> Ty -> * where
  Var   :: Elem ctx ty -> Exp ctx ty
  Lam   :: Exp (arg ': ctx) res -> Exp ctx (arg :> res)
  App   :: Exp ctx (arg :> res) -> Exp ctx arg -> Exp ctx res
  Arith :: Exp ctx I -> ArithOp ty -> Exp ctx I -> Exp ctx ty
  Cond  :: Exp ctx B -> Exp ctx ty -> Exp ctx ty -> Exp ctx ty
  Fix   :: Exp ctx (ty :> ty) -> Exp ctx ty
  IntE  :: Int -> Exp ctx I
  BoolE :: Bool -> Exp ctx B
  Pair  :: Exp ctx a -> Exp ctx b -> Exp ctx (P a b)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented May 31, 2017

castWith :: (a :~: b) -> a -> b
Source

Type-safe cast, using propositional equality

gcastWith :: (a :~: b) -> (a ~ b => r) -> r
Source

Generalized form of type-safe cast using propositional equality

apply :: (f :: g) -> (a :: b) -> f a :~: g b
Source

Apply one equality to another, respectively

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented May 31, 2017

2.2 Functions are functors
Now we wish to establish that functions f : A → B behave functorially on paths. In traditional
type theory, this is equivalently the statement that functions respect equality. Topologically, this
corresponds to saying that every function is “continuous”, i.e. preserves paths.
Lemma 2.2.1. Suppose that f : A → B is a function. Then for any x, y : A there is an operation
apf
: (x =A y) → (f(x) =B f(y)).
Moreover, for each x : A we have apf
(reflx) ≡ reflf(x)
.

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 2, 2017

https://github.com/robeverest/ast-decoration/blob/20c47f0cbe946fc3f32a23e6989f5b415dd80df3/Substitution.hs#L125

-- Weakening
-- =============================================================
--
-- Weakening is the process of changing a term's environment to one greater
-- than or equal in size to the original. Operationally, this means changing
-- the value of the debruijn indices in the term via a mapping. We capture
-- this mapping with 'env :> env'', which is a function from indices in 'env'
-- to indices in 'env''
--
-- The process of renaming debruijn indices in a term, naturally requires
-- traversal of the entire term. This feels like a weakness of our
-- representation. In other representations, weakening is either constant time
-- or not necessary. However, we can amortise the cost of weakening to be
-- constant time by delaying it and performing many weakenings in bulk.
-- See 'Decoration'.
--
type env :> env' = forall t. Idx env t -> Idx env' t

-- | All things that can be weakened. We keep this as a separate typeclass and
-- not just a function defined in terms of 'substitute' as there are instances
-- when something can be weakened but cannot be rebuilt.
--
class Sink stlc where
  weaken :: env :> env' -> stlc env t -> stlc env' t
  default weaken :: Substitutable stlc => env :> env' -> stlc env t -> stlc env' t
  weaken v = substitute (varIn . v)

instance Sink Idx where
  weaken v = v

-- Both of these instances can be defined in terms of substitute.
--
instance (Substitutable stlc, InnerSyntax stlc ~ PreOpenSTLC stlc) => Sink (PreOpenSTLC stlc) where
instance Sink OpenSTLC where

-- Inlining
--
inline :: forall a env t. OpenSTLC (a ': env) t -> OpenSTLC env a -> OpenSTLC env t
inline a (OpenSTLC b) = substitute f a
  where
    f :: forall t. Typeable t 
      => Idx (a ': env) t
      -> PreOpenSTLC OpenSTLC env t
    f ZeroIdx      = b
    f (SuccIdx ix) = Var ix

type env :?> env' = forall t. Idx env t -> Maybe (Idx env' t)

strengthen :: env :?> env' -> OpenSTLC env t -> Maybe (OpenSTLC env' t)
strengthen v = reconstruct (fmap Var . v)

Functors??

newtype Kleisli f env env' = Kleisli (forall t. f env t -> Maybe (f env' t))

fmap :: (env :?> env') -> Kleisli (OpenSTLC env) (OpenSTCL env')
...????
weaken :: Sink stlc => env :> env' -> stlc env t -> stlc env' t

verify when on computer

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 2, 2017

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 5, 2017

https://www.reddit.com/r/haskell/comments/6fcl9z/universally_stateless_monads/

(\\) is fmap

type f <~ g = forall xx. g xx -> f xx

newtype Foo :: Constraint -> Type -> Type where
  Foo :: (ctx => a) -> Foo ctx a

(//) :: (ctx :- ctx') -> (Foo ctx <~ Foo ctx')
Sub dict // Foo r = Foo
  (withDict dict r)

Something like

type (<~) = Op (Nat (->) (->))

instance Functor Foo where
  type Dom Foo = (:-)
  type Cod Foo = (<~)

  fmap :: (ctx :- ctx) -> (Foo ctx <~ Foo ctx')
  fmap (Sub dict) = Op $ Nat $ \(Foo r) -> Foo (withDict dict r)
@Icelandjack

This comment has been minimized.

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jul 25, 2017

Using Linear, almost

newtype M :: Nat -> Nat -> Type -> Type where
  M :: V n (V m a) -> M n m a

tr :: Dim m => M n m a -> M m n a 
tr (M xss) = M (transpose xss)

aa :: (KnownNat m, Num a) => M n m a -> V m a -> V n a
M xss `aa` x = xss !* x
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 28, 2017

Maybe dropEnv :: Env m ys -> SubList xs ys -> Env m xs from https://github.com/goldfirere/thesis/blob/master/effects/Effects.hs#L146

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Sep 17, 2017

mapMaybe :: Kleisli Maybe a b -> ([a] -> [b])

https://hackage.haskell.org/package/witherable-0.2/docs/Data-Witherable.html

Formally, the class Filterable represents a functor from Kleisli Maybe to Hask.

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Sep 28, 2017

newtype Not a = Not (a -> Void)

modusTollens :: (b -> a) -> (Not a -> Not b)
modusTollens f (Not to_void) = Not (to_void . f)
newtype Not a = Not (Op Void a)

modusTollens :: forall a b. (b -> a) -> (Not a -> Not b)
modusTollens = coerce (contramap @(Op Void) @b @a)

http://www.michaelburge.us/2017/09/27/delta-debugging-in-haskell.html

  • Contravariant generalizes Modus Tollens .
  • Divisible generalizes Conjunction Introduction .
  • Decidable generalizes Disjunction Elimination .
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 2, 2017

http://www.haskellforall.com/2012/09/the-functor-design-pattern.html

class (Category (Dom f), Category (Cod f)) => Varpi (f :: i -> j) where
  type Dom f :: Cat i
  type Cod f :: Cat j

  varpa :: Dom f a a' -> Cod f (f a) (f a')

newtype Lift :: (Type -> Type) -> (Type -> Type) where
  Lift :: a -> Lift m a

instance Monad m => Varpi (Lift m) where
  type Dom (Lift m) = (->)
  type Cod (Lift m) = Kleisli m

  varpa :: (a -> a') -> Kleisli m (Lift m a) (Lift m a')
  varpa f = Kleisli $ \(Lift a) -> pure (Lift (f a))
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 2, 2017

Not sure how to model monoid homomorphisms as functors, we really need type families () -> ()

newtype MonCat :: Type -> Cat () where
  MCat :: m -> MonCat m a b

instance Monoid m => Category (MonCat m) where
  id = MCat mempty

  MCat f . MCat g = MCat (mappend f g)
-- NOT ALLOWED
data Hom :: Type -> (() -> ())

instance Functor (Hom a) where
  type Dom (Hom a) = MonCat [a]
  type Cod (Hom a) = MonCat (Sum Int)

  fmap :: MonCat [a] b b' -> MonCat (Sum Int) (Hom a b) (Hom a b')
  fmap (MCat xs) = MCat (Sum (length xs))

and

fmap_concat :: MonCat [[a]] b b' -> MonCat [a] b b'
fmap_concat (MCat xss) = MCat (concat xss)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 2, 2017

type f ~~~> g = forall xx yy zz. f xx yy zz -> g xx yy zz

data IIteratee :: Type -> (Type -> Type) -> (Type -> Type)
data EIteratee :: Type -> (Type -> Type) -> (Type -> Type)

instance Functor (IIteratee a b)
instance Applicative (IIteratee a b)
instance Monad (IIteratee a b)

instance Functor (EIteratee a b)
instance Applicative (EIteratee a b)
instance Monad (EIteratee a b)

morph :: IIteratee ~~~> EIteratee
morph = undefined

newtype I (s :: Type) (m :: Type -> Type) a = I { getI :: a }

instance Varpi (I s m) where
  type Dom (I s m) = Kleisli (IIteratee s m)
  type Cod (I s m) = Kleisli (EIteratee s m)

  varpa :: forall a a'. Kleisli (IIteratee s m) a a' -> Kleisli (EIteratee s m) (I s m a) (I s m a')
  varpa (Kleisli arr) =
    Kleisli $ \(I a) -> morph (I <$> arr a)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 2, 2017

https://gist.github.com/paf31/f3204cc5d76e6dd6f611

newtype MFun :: Type -> Cat Du where
  MFun :: m -> MFun m a b

instance Monoid m => Category (MFun m) where
  id = MFun mempty

  MFun m . MFun n = MFun (mappend m n)

newtype Realize :: Type -> Du -> Type where
  Realize :: m -> Realize m a

instance Monoid m => Varpi (Realize m) where
  type Dom (Realize m) = MFun m
  type Cod (Realize m) = (->)

  varpa :: MFun m a a' -> (Realize m a -> Realize m a')
  varpa (MFun m) (Realize m2) = Realize (mappend m m2)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 9, 2017

https://hackage.haskell.org/package/free-functors-0.8.1/docs/src/Data-Functor-Free.html

type Transform ctx a b = forall xx. ctx xx => (b -> xx) -> (a -> xx)

transform :: Transform ctx a b -> ((Free ctx) a -> (Free ctx) b)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 18, 2017

https://www.win.tue.nl/~japie/dp/general/Haskell.pdf

newtype Circuit a b = Circuit { unCircuit :: a -> (Circuit a b, b) }

instance Category Circuit where
  id :: Circuit a a
  id = Circuit $ (id, )

  (.) :: Circuit b c -> Circuit a b -> Circuit a c
  Circuit cir2 . Circuit cir1 = Circuit $ \(cir1 -> (cir1', cir2 -> (cir2', value))) ->
    (cir2' . cir1', value)

-- Do laws hold?
instance Functor [] where
  type Dom [] = Circuit 
  type Cod [] = (->)

  fmap :: Circuit a a' -> ([a] -> [a'])
  fmap cir = snd . mapAccumL unCircuit cir

Causal Commutative Arrows and Their Optimization

newtype SF a b = SF (a -> (b, SF a b))

instance Functor [] where
  type Dom [] = SF
  type Cod [] = (->)

  runSF :: SF a b -> ([a] -> [b])
  runSF ...
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 19, 2017

data (...) :: Cat Type where
  Nil   :: a...a
  (:::) :: a...b -> b...c -> a...c

instance Category (...) where
  id :: a...a
  id = Nil

  (.) :: b...c -> a...b -> a...c
  as . Nil      = as
  as . (b:::bs) = b ::: (as . bs)

we can lift any functor to the unbiased presentation this https://gist.github.com/Icelandjack/899ccf151d689bf8208918038b4d7c4c#gistcomment-2233512

newtype Unbias f a = Unbias (f a)

instance FunctorOf (->) (->) f => Functor (Unbias f) where
  type Dom (Unbias f) = (...)
  type Cod (Unbias f) = (...)

  fmap :: a...a' -> Unbias f a...Unbias f a'
  fmap = \case
    Nil -> 
      Nil

    f:::fs -> 
      fmap f:::fmap f fs
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 20, 2017

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 26, 2017

https://github.com/msp-strath/platypus/blob/61b721337c3f5530f293ae89238371fa488426c5/September17/Utils.hs

data LStar r a b where
  L0    :: LStar r a a
  (:<:) :: LStar r a b -> r b c -> LStar r a c

-- fmap
lextend :: (forall a b . r a b -> LStar s a b) -> LStar r a b  -> LStar s a b
lextend f L0 = L0
lextend f (xs :<: x) = lextend f xs >>> f x

-- fmap
lmap :: (forall a b . r a b -> s a b) -> LStar r a b  -> LStar s a b
lmap f xs = lextend (\ x -> L0 :<: f x) xs
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 8, 2017

I'm intrigued by types wrapping type families

type family
  F (bool :: Bool) :: Type -> Type where
  F False = Maybe
  F True  = []

newtype Ty bool a = Ty (F bool a)

instance SingI (bool :: Bool) => Functor (Ty bool) where
  fmap :: (a -> a') -> (Ty bool a -> Ty bool a')
  fmap f (Ty xs) =
    case sing @Bool @bool of
      SFalse -> Ty (fmap f xs)
      STrue  -> Ty (fmap f xs)

and I don't have a good intuition for what kind of functor Ty would be

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 8, 2017

If we assume Cod Ty = Nat (->) (->) is the functor category, then arrows in Ty bool ~> Ty bool' basically one of

Maybe ~> Maybe
Maybe ~> []
[]    ~> Maybe
[]    ~> []

depending on bool, bool' and the Dom Ty = (-?>):

fmap :: (bool -?> bool') -> (Ty bool ~> Ty bool')
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 8, 2017

We actually have a choice between

newtype Ty :: Bool -> Type -> Type where
  Ty :: F bool a -> Ty bool a

instance pi (bool :: Bool) => Functor (Ty bool)

or (ideally, marking F as injective)

data Ty bool a where
  Ty :: Functor (F bool) => F bool a -> Ty bool a

instance Functor (Ty bool)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 11, 2017

http://adam.gundry.co.uk/pub/thesis/thesis-2013-12-03.pdf

wait :: (n <= m) => (Cost n a -> Cost m a)
wait (Hide a) = Hide a
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 11, 2017

{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-}

import Data.Kind
import Data.Singletons
import Data.Singletons.TH

type Cat ob = ob -> ob -> Type

singletons 
  [d| 
  idd x = x
  comp f g a = f (g a)
  konst a b = a
  |]

type (·) = CompSym2
type ID = IddSym0

class Varpi (f :: i ~> j) where
  type Dom (f :: i ~> j) :: Cat i
  type Cod (f :: i ~> j) :: Cat j

  varpa :: Dom f a a' -> Cod f (f@@a) (f@@a')

instance Varpi (IddSym0 :: Type ~> Type) where
  type Dom (IddSym0 :: Type ~> Type) = (->)
  type Cod (IddSym0 :: Type ~> Type) = (->)

  varpa :: (a -> a') -> (a -> a')
  varpa = id

instance Varpi (KonstSym1 f::Type ~> Type) where
  type Dom (KonstSym1 f::Type ~> Type) = (->)
  type Cod (KonstSym1 f::Type ~> Type) = (->)
  
  varpa :: (a -> a') -> (f -> f)
  varpa _ = id

class    (Varpi f, Dom f ~ dom, Cod f ~ cod) => VarpiOf dom cod f 
instance (Varpi f, Dom f ~ dom, Cod f ~ cod) => VarpiOf dom cod f 

instance (VarpiOf (->) (->) f, VarpiOf (->) (->) g) => Varpi (CompSym2 f g::Type~>Type) where
  type Dom (CompSym2 f g::Type ~> Type) = (->)
  type Cod (CompSym2 f g::Type ~> Type) = (->)

  varpa :: forall a a'. (a -> a') -> (f@@(g@@a) -> f@@(g@@a'))
  varpa = varpa @_ @_ @f . varpa @_ @_ @g
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 14, 2017

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

type MapSym f g = forall xx. f (Full xx) -> g (Full xx)

mapArgs :: MapSym f f' -> (Args f ~> Args f')
mapArgs _ Nil     = Nil
mapArgs f (a:*as) = f a :* mapArgs f as
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 17, 2017

data Len     :: Type -> Type -> () S.~> ()
data FoldMap :: (a S.~> m) -> (Type -> Type) -> () S.~> ()

type instance S.Apply (Len     a num) unit = unit
type instance S.Apply (FoldMap inj f) unit = unit

data M :: Type -> Cat () where
  M :: { unM :: m } -> M m '() '()

class Func (f::k S.~> k') where
  type Dom f :: Cat k
  type Cod f :: Cat k'

  mp :: Dom f a a' -> Cod f (f@@a) (f@@a')

instance (Monoid m, Num num) => Func (Len a num) where
  type Dom (Len a num) = (M [a] :: Cat ())
  type Cod (Len a num) = (M (M.Sum num) :: Cat ())

  mp :: M [a] unit unit' -> M (M.Sum num) unit unit'
  mp (M xs) = M (M.Sum (fromIntegral (length xs)))

type GoodKind a = (SingKind a, Demote a ~ a)

instance (SingI inj, GoodKind a, GoodKind mon, Foldable f, Monoid mon) => Func (FoldMap (inj::a S.~> mon) f) where
  type Dom (FoldMap (inj::a S.~> mon) f) = (M (f a) :: Cat ())
  type Cod (FoldMap (inj::a S.~> mon) f) = (M mon   :: Cat ())

  mp :: M (f a) unit unit' -> M mon unit unit'
  mp (M fa) = M (foldMap f fa) where

    f :: a -> mon
    f = fromSing (sing @_ @inj)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 17, 2017

data Len     :: Type -> Type -> () S.~> ()
data FoldMap :: (a S.~> m) -> (Type -> Type) -> () S.~> ()

type instance S.Apply (Len     a num) unit = unit
type instance S.Apply (FoldMap inj f) unit = unit

data M :: Type -> Cat () where
  M :: { unM :: m } -> M m '() '()

class Func (f::k S.~> k') where
  type Dom f :: Cat k
  type Cod f :: Cat k'

  mp :: Dom f a a' -> Cod f (f@@a) (f@@a')

instance (Monoid m, Num num) => Func (Len a num) where
  type Dom (Len a num) = (M [a] :: Cat ())
  type Cod (Len a num) = (M (M.Sum num) :: Cat ())

  mp :: M [a] unit unit' -> M (M.Sum num) unit unit'
  mp (M xs) = M (M.Sum (fromIntegral (length xs)))

type GoodKind a = (SingKind a, Demote a ~ a)

instance (SingI inj, GoodKind a, GoodKind mon, Foldable f, Monoid mon) => Func (FoldMap (inj::a S.~> mon) f) where
  type Dom (FoldMap (inj::a S.~> mon) f) = (M (f a) :: Cat ())
  type Cod (FoldMap (inj::a S.~> mon) f) = (M mon   :: Cat ())

  mp :: M (f a) unit unit' -> M mon unit unit'
  mp (M fa) = M (foldMap f fa) where

    f :: a -> mon
    f = fromSing (sing @_ @inj)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 19, 2017

class Varpi (f::k ~> k') where
  type Dom f :: k  ~> k  ~> Type
  type Cod f :: k' ~> k' ~> Type

  varpa :: Dom f@@a@@a' -> Cod f@@(f@@a)@@(f@@a')

data Dup    :: Type ~> Type
data Pair2  :: Type ~> Type ~> Type
data Pair2' :: Type -> Type ~> Type

type instance Apply Dup a = (a, a)

type instance Apply Pair2      a = Pair2' a
type instance Apply (Pair2' a) b = (a -> b, a -> b)

instance Varpi Dup where
  type Dom Dup = Pair2
  type Cod Dup = TyCon2 (->)

  varpa :: (a -> b, a -> b) -> ((a, a) -> (b, b))
  varpa (f, f') (a, a') = (f a, f' a')
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 19, 2017

class Varpi (f::k ~> k') where
  type Dom f :: Cat k
  type Cod f :: Cat k'

  varpa :: Dom f@@a@@a' -> Cod f@@(f@@a)@@(f@@a')

data Dup   :: (Type, Type) ~> (Type, Type)
data Arrs  :: (Type, Type) ~> (Type, Type) ~> Type
data Arrs' :: (Type, Type) -> (Type, Type) ~> Type

type family 
  First (pair :: (a, b)) :: a where
  First '(a, _) = a

type family 
  Latter (pair :: (a, b)) :: b where
  Latter '(_, b) = b

data ARRS :: Cat i -> (i, i) ~> i

type instance Apply (ARRS cat) '(a, b) = (a, b)

data Arrows :: Cat i -> Cat j -> Cat (i, j) where
  Arrows 
    :: cat  a  b
    -> cat' a' b'
    -> Arrows cat cat' '(a, b) '(a', b')

instance (->) ~ cat => Varpi (ARRS cat) where
  type Dom (ARRS cat) = TyCon2 (Arrows cat cat)
  type Cod (ARRS cat) = TyCon2 cat 

  varpa (Arrows f f') (a, a') = (f a, f' a')

https://ghc.haskell.org/trac/ghc/ticket/7259 ( Eta expansion of products in System FC )

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 20, 2017

data DUP :: Cat k -> k ~> (k, k)                                                                                                                                                
                                                                                                                                                                                
type instance Apply (DUP cat) a = '(a, a)                                                                                                                                       
                                                                                                                                                                                
instance Varpi (DUP cat::k ~> (k, k)) where                                                                                                                                     
  type Dom (DUP cat) = cat                                                                                                                                                      
  type Cod (DUP cat) = Arrs cat                                                                                                                                                 
                                                                                                                                                                                
  (<$>) :: cat a a' -> Arrs cat '(a, a) '(a', a')                                                                                                                               
  (<$>) f = Arrs f f                                                                                                                                                            
                                                                                                                                                                                
data Arrs :: Cat k -> Cat (k, k) where                                                                                                                                          
  Arrs :: cat a b -> cat a' b'                                                                                                                                                  
       -> Arrs cat '(a, a') '(b, b')                                                                                                                                            
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 20, 2017

data DUP :: Cat k -> k ~> (k, k)                                                                                                                                                
                                                                                                                                                                                
type instance Apply (DUP cat) a = '(a, a)                                                                                                                                       
                                                                                                                                                                                
instance Varpi (DUP cat::k ~> (k, k)) where                                                                                                                                     
  type Dom (DUP cat) = cat                                                                                                                                                      
  type Cod (DUP cat) = Arrs cat                                                                                                                                                 
                                                                                                                                                                                
  (<$>) :: cat a a' -> Arrs cat '(a, a) '(a', a')                                                                                                                               
  (<$>) f = Arrs f f                                                                                                                                                            
                                                                                                                                                                                
data Arrs :: Cat k -> Cat (k, k) where                                                                                                                                          
  Arrs :: cat a b -> cat a' b'                                                                                                                                                  
       -> Arrs cat '(a, a') '(b, b')                                                                                                                                            
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 20, 2017

singletons [d| data N=O|S N |]

data V :: N -> Type -> Type where
  VNil  :: V O a
  VCons :: a -> V n a -> V (S n) a

data instance Sing (sing:: V n a) where
  SVNil  :: Sing (VNil::V O a)
  SVCons :: Sing (x::a) -> Sing (xs::V n a) -> Sing (VCons x xs::V (S n) a)

------

data Arrs :: Cat k -> forall n. Cat (V n k) where
  ArrsNil :: Arrs cat 'VNil 'VNil

  ArrsCons :: cat a b
           -> Arrs cat as bs
           -> Arrs cat ('VCons a as) ('VCons b bs)

data Dup (n::N) :: Cat k -> k ~> V n k

type instance Apply (Dup n cat) a = Pure a

class PPointed (n::N) where
  type Pure (a::k) :: V n k

class SingI n => SPointed (n::N) where
  sPure :: Sing (a::k) -> Sing (Pure a::V n k)

instance SPointed O where
  sPure :: Sing (a::k) -> Sing (Pure a::V O k)
  sPure _ = SVNil

instance SPointed n => SPointed (S n) where
  sPure :: Sing (a::k) -> Sing (Pure a::V (S n) k)
  sPure sing = SVCons sing (sPure sing)

instance PPointed (O::N) where
  type Pure (a::k) = VNil

instance PPointed n => PPointed (S n::N) where
  type Pure (a::k) = VCons a (Pure a)

instance SingI n => Varpi (Dup (n::N) cat) where
  type Dom (Dup (n::N) cat) = cat
  type Cod (Dup (n::N) cat) = Arrs cat

  fmap :: cat a a' -> Arrs cat (Pure a) (Pure a')
  fmap f = 
    case sing :: Sing n of
      SO             -> ArrsNil
      SS (m::Sing m) -> withSingI m
        (ArrsCons f (fmap @(Dup m cat) f))
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 24, 2017

newtype GrpOb = MkGrpOb Type

data Grp :: Cat GrpOb where
  Grp :: (a -> b) -> {- ... proof that it is group -} -> Grp (MkGrpOb a) (MkGrpOb b)

data Forgetful :: GRP ~> Type

type instance Forgetful · MkGrpOb a = a

instance Functor Forgetful where
  type Dom Forgetful = Grp
  type Cod Forgetful = (->)

  fmap :: Grp a a' -> (Forgetful·a -> Forgetful·a')
  fmap (Grp f {- .. -}) = f
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Dec 1, 2017

data E :: Type -> Type where
  Lam :: (E a -> E b) -> E (a -> b)
  App :: E (a -> b) -> (E a -> E b)

newtype a :-- b where
  Arrow :: E (a -> b) -> (a :-- b)

instance Category (:--) where
  id :: a :-- a
  id = Arrow (Lam id)

  (.) :: (b :-- c) -> (a :-- b) -> (a :-- c)
  Arrow f . Arrow g = Arrow $ Lam (App f . App g)

instance Functor (:--) where
  type Dom (:--) = Y (:--)
  type Cod (:--) = Nat (:--) (->)

  fmap :: Y (:--) a a' -> Nat (:--) (->) ((:--) a) ((:--) a')
  fmap (Y f) = Nat (. f)

instance Functor ((:--) a) where
  type Dom ((:--) a) = (:--)
  type Cod ((:--) a) = (->)

  fmap :: (b :-- b') -> ((a:--b) -> (a:--b'))
  fmap = (.)

we get

instance Functor E where
  type Dom E = (:--)
  type Cod E = (->)

  fmap :: (a :-- a') -> (E a -> E a')
  fmap (Arrow f) = App f

instance FullyFaithful E where
  unmap :: (E a -> E a') -> (a :-- a')
  unmap = Arrow . Lam
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Dec 4, 2017

https://pdfs.semanticscholar.org/cd67/f6efb6e9a037d25006631cb1b9909c4e9ca5.pdf
FUNCTOR: subst :: Subst gamma delta -> (Exp delta a -> Exp gamma a)

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Dec 6, 2017

Lenses for Web Data

Functor from Lens to Hask (also Applicative)

For our purposes, we will need to generalize its definition slightly 3 to consider functors from other categories (such as Bij and Lens) to Hask.

-- instance Functor F where
--   type Dom F = Lens
--   type Cod F = (->)

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

```haskell
class LApplicative f where
  lpure :: a -> f a
  lapp :: f (Lens a b) -> (f a -> f b)

Functors on categories other than Hask have appeared in other contexts. Functors over isomor-
phisms are used in the fclabels library [VHEV12]. However, fclabels also provides an applicative
functor interface, which can be used to produce intuitively incorrect bidirectional transforma-
tions. Similarly, functors over partial isomorphisms from Iso to Hask are essential in Rendel
and Ostermann’s invertible syntax descriptions [RO10]. They also employ a variant of Monoidal
functors (which they call ProductFunctors). A natural question for further work is whether
Monoidal functors over partial isomorphisms suffice for invertible syntax descriptions, so that
one can easily compose parser or pretty-printer combinators with formlenses. To the best of our
knowledge, we are the first to use (monoidal) functors over lenses for programming.

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Dec 27, 2017

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

This comment has been minimized.

@Icelandjack

This comment has been minimized.

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Apr 8, 2018

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

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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jul 22, 2018

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Oct 17, 2018

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack 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

This comment has been minimized.

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