aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/spec
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/spec')
-rw-r--r--stdlib/source/spec/lux/abstract/functor/contravariant.lux31
1 files changed, 31 insertions, 0 deletions
diff --git a/stdlib/source/spec/lux/abstract/functor/contravariant.lux b/stdlib/source/spec/lux/abstract/functor/contravariant.lux
new file mode 100644
index 000000000..b21e28e68
--- /dev/null
+++ b/stdlib/source/spec/lux/abstract/functor/contravariant.lux
@@ -0,0 +1,31 @@
+(.module:
+ [lux #*
+ [abstract
+ [equivalence (#+ Equivalence)]
+ [monad (#+ do)]]
+ [data
+ [number
+ ["n" nat]]]
+ [control
+ ["." function]]
+ [math
+ ["." random]]
+ ["_" test (#+ Test)]]
+ {1
+ ["." / (#+ Functor)]})
+
+(def: (identity equivalence value (^open "/@."))
+ (All [f a] (-> (Equivalence (f a)) (f a) (Functor f) Test))
+ (_.test "Law of identity."
+ (equivalence
+ (/@map function.identity value)
+ value)))
+
+(def: #export (spec equivalence value functor)
+ (All [f a] (-> (Equivalence (f a)) (f a) (Functor f) Test))
+ (do random.monad
+ [sample random.nat]
+ (<| (_.with-cover [/.Functor])
+ ($_ _.and
+ (..identity equivalence value functor)
+ ))))