1 files changed, 61 insertions, 0 deletions
diff --git a/stdlib/source/spec/lux/abstract/comonad.lux b/stdlib/source/spec/lux/abstract/comonad.lux
new file mode 100644
index 000000000..3dfda0bbf
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/comonad.lux
@@ -0,0 +1,61 @@
+(.module:
+  [lux #*
+   [abstract
+    [monad (#+ do)]]
+   [data
+    [number
+     ["n" nat]]]
+   [math
+    ["." random]]
+   ["_" test (#+ Test)]]
+  {1
+   ["." / (#+ CoMonad)]}
+  [//
+   [functor (#+ Injection Comparison)]])
+
+(def: (left-identity injection (^open "_@."))
+  (All [f] (-> (Injection f) (CoMonad f) Test))
+  (do {@ random.monad}
+    [sample random.nat
+     morphism (:: @ map (function (_ diff)
+                          (|>> _@unwrap (n.+ diff)))
+                  random.nat)
+     #let [start (injection sample)]]
+    (_.test "Left identity."
+            (n.= (morphism start)
+                 (|> start _@split (_@map morphism) _@unwrap)))))
+
+(def: (right-identity injection comparison (^open "_@."))
+  (All [f] (-> (Injection f) (Comparison f) (CoMonad f) Test))
+  (do random.monad
+    [sample random.nat
+     #let [start (injection sample)
+           == (comparison n.=)]]
+    (_.test "Right identity."
+            (== start
+                (|> start _@split (_@map _@unwrap))))))
+
+(def: (associativity injection comparison (^open "_@."))
+  (All [f] (-> (Injection f) (Comparison f) (CoMonad f) Test))
+  (do {@ random.monad}
+    [sample random.nat
+     increase (:: @ map (function (_ diff)
+                          (|>> _@unwrap (n.+ diff)))
+                  random.nat)
+     decrease (:: @ map (function (_ diff)
+                          (|>> _@unwrap(n.- diff)))
+                  random.nat)
+     #let [start (injection sample)
+           == (comparison n.=)]]
+    (_.test "Associativity."
+            (== (|> start _@split (_@map (|>> _@split (_@map increase) decrease)))
+                (|> start _@split (_@map increase) _@split (_@map decrease))))))
+
+(def: #export (spec injection comparison monad)
+  (All [f] (-> (Injection f) (Comparison f) (CoMonad f) Test))
+  (<| (_.with-cover [/.CoMonad])
+      ($_ _.and
+          (..left-identity injection monad)
+          (..right-identity injection comparison monad)
+          (..associativity injection comparison monad)
+          )))