• API
• FAQ
• Tools
• Archive
SHARE
TWEET

Untitled

a guest Apr 20th, 2019 80 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. :: :: morphism c = c -> c -> *
2.
3. :: :: morphism c -> *
4. :: category p =
5. ::   { id: p a a, compose: p b c -> p a b -> p a c }
6.
7. :: :: (c -> d) -> morphism c -> morphism d -> *
8. :: functor f i o =
9. ::   { map: i a b -> o (f a) (f b) }
10.
11. :: :: morphism c -> morphism c
12. :: opposite i a b = i b a
13.
14. :: :: morphism c -> morphism d -> morphism (c, d)
15. :: product c d (a, b) (s, t) = (c a s, d b t)
16.
17. :: :: morphism c -> ((c, c) -> *) -> *
18. :: profunctor c p = functor p (product (opposite c) c) (->)
19.
20. :: :: (a -> b -> c) -> (a, b) -> c
21. :: uncurry f (a, b) = f a b
22.
23. :: :: morphism * -> *
24. :: setProfunctor p = profunctor (->) (Uncurry p)
25.
26. -- We can inline this step by step to see what type we get
27. -- > profunctor (->) (uncurry p)
28. --
29. -- > functor (uncurry p) x (->)
30. --   where
31. --   x = product (opposite (->)) (->)
32. --     = \(a, b) (s, t) -> (opposite (->) a s, (->) b t)
33. --     = \(a, b) (s, t) -> ((->) s a, (->) b t)
34. --     = \(a, b) (s, t) -> (s -> a, b -> t)
35. --
36. -- > { map: i a b -> o (f a) (f b) }
37. --   where
38. --   f = uncurry p
39. --   i = x
40. --   o = (->)
41. --   x = \(a, b) (s, t) -> (s -> a, b -> t)
42. --
43. -- > { map: x (a, b) (s, t) -> f (a, b) -> f (s, t) }
44. --   where
45. --   f = uncurry p
46. --   x = \(a, b) (s, t) -> (s -> a, b -> t)
47. --
48. -- > { map: (s -> a, b -> t) -> p a b -> p s t }
49.
50. :: setProfunctor (->)
51. fnProfunctor = { map: \(l, r) f -> r . f . l }
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.
Not a member of Pastebin yet?