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. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top