Advertisement
Guest User

Untitled

a guest
Apr 20th, 2019
108
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.30 KB | None | 0 0
  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 }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement