From ce7614f00a134cb61b4a6f88cfea33461a7bf478 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 7 Oct 2020 17:00:57 -0400 Subject: Test imports for circular dependencies. --- stdlib/source/spec/lux/abstract/comonad.lux | 61 +++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 stdlib/source/spec/lux/abstract/comonad.lux (limited to 'stdlib/source/spec') 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) + ))) -- cgit v1.2.3