Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- :: :: morphism c = c -> c -> *
- :: :: morphism c -> *
- :: category p =
- :: { id: p a a, compose: p b c -> p a b -> p a c }
- :: :: (c -> d) -> morphism c -> morphism d -> *
- :: functor f i o =
- :: { map: i a b -> o (f a) (f b) }
- :: :: morphism c -> morphism c
- :: opposite i a b = i b a
- :: :: morphism c -> morphism d -> morphism (c, d)
- :: product c d (a, b) (s, t) = (c a s, d b t)
- :: :: morphism c -> ((c, c) -> *) -> *
- :: profunctor c p = functor p (product (opposite c) c) (->)
- :: :: (a -> b -> c) -> (a, b) -> c
- :: uncurry f (a, b) = f a b
- :: :: morphism * -> *
- :: setProfunctor p = profunctor (->) (Uncurry p)
- -- We can inline this step by step to see what type we get
- -- > profunctor (->) (uncurry p)
- --
- -- > functor (uncurry p) x (->)
- -- where
- -- x = product (opposite (->)) (->)
- -- = \(a, b) (s, t) -> (opposite (->) a s, (->) b t)
- -- = \(a, b) (s, t) -> ((->) s a, (->) b t)
- -- = \(a, b) (s, t) -> (s -> a, b -> t)
- --
- -- > { map: i a b -> o (f a) (f b) }
- -- where
- -- f = uncurry p
- -- i = x
- -- o = (->)
- -- x = \(a, b) (s, t) -> (s -> a, b -> t)
- --
- -- > { map: x (a, b) (s, t) -> f (a, b) -> f (s, t) }
- -- where
- -- f = uncurry p
- -- x = \(a, b) (s, t) -> (s -> a, b -> t)
- --
- -- > { map: (s -> a, b -> t) -> p a b -> p s t }
- :: setProfunctor (->)
- fnProfunctor = { map: \(l, r) f -> r . f . l }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement