diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/test/lux/abstract/monad.lux | 109 |
1 files changed, 79 insertions, 30 deletions
diff --git a/stdlib/source/test/lux/abstract/monad.lux b/stdlib/source/test/lux/abstract/monad.lux index ecb292afb..4d85a6e90 100644 --- a/stdlib/source/test/lux/abstract/monad.lux +++ b/stdlib/source/test/lux/abstract/monad.lux @@ -1,61 +1,110 @@ (.module: [lux #* [data + ["." identity (#+ Identity)] [number ["n" nat]] - [text - ["%" format (#+ format)]]] - [control - ["." function]] + [collection + ["." list ("#@." functor fold)]]] [math - ["r" random]] + ["." random]] ["_" test (#+ Test)]] {1 ["." / (#+ Monad do)]} [// [functor (#+ Injection Comparison)]]) -(def: (left-identity injection comparison (^open "_;.")) +(def: (left-identity injection comparison (^open "_@.")) (All [f] (-> (Injection f) (Comparison f) (Monad f) Test)) - (do r.monad - [sample r.nat + (do random.monad + [sample random.nat morphism (:: @ map (function (_ diff) - (|>> (n.+ diff) _;wrap)) - r.nat)] + (|>> (n.+ diff) _@wrap)) + random.nat)] (_.test "Left identity." ((comparison n.=) - (|> (injection sample) (_;map morphism) _;join) + (|> (injection sample) (_@map morphism) _@join) (morphism sample))))) -(def: (right-identity injection comparison (^open "_;.")) +(def: (right-identity injection comparison (^open "_@.")) (All [f] (-> (Injection f) (Comparison f) (Monad f) Test)) - (do r.monad - [sample r.nat] + (do random.monad + [sample random.nat] (_.test "Right identity." ((comparison n.=) - (|> (injection sample) (_;map _;wrap) _;join) + (|> (injection sample) (_@map _@wrap) _@join) (injection sample))))) -(def: (associativity injection comparison (^open "_;.")) +(def: (associativity injection comparison (^open "_@.")) (All [f] (-> (Injection f) (Comparison f) (Monad f) Test)) - (do r.monad - [sample r.nat + (do random.monad + [sample random.nat increase (:: @ map (function (_ diff) - (|>> (n.+ diff) _;wrap)) - r.nat) + (|>> (n.+ diff) _@wrap)) + random.nat) decrease (:: @ map (function (_ diff) - (|>> (n.- diff) _;wrap)) - r.nat)] + (|>> (n.- diff) _@wrap)) + random.nat)] (_.test "Associativity." ((comparison n.=) - (|> (injection sample) (_;map increase) _;join (_;map decrease) _;join) - (|> (injection sample) (_;map (|>> increase (_;map decrease) _;join)) _;join))))) + (|> (injection sample) (_@map increase) _@join (_@map decrease) _@join) + (|> (injection sample) (_@map (|>> increase (_@map decrease) _@join)) _@join))))) (def: #export (spec injection comparison monad) (All [f] (-> (Injection f) (Comparison f) (Monad f) Test)) - (_.context (%.name (name-of /.Monad)) - ($_ _.and - (..left-identity injection comparison monad) - (..right-identity injection comparison monad) - (..associativity injection comparison monad) - ))) + (<| (_.with-cover [/.Monad]) + ($_ _.and + (..left-identity injection comparison monad) + (..right-identity injection comparison monad) + (..associativity injection comparison monad) + ))) + +(def: #export test + Test + (do random.monad + [mono random.nat + poly (random.list 10 random.nat)] + (<| (_.covering /._) + ($_ _.and + (_.cover [/.do] + (n.= (inc mono) + (: (Identity Nat) + (/.do identity.monad + [sample (wrap mono)] + (wrap (inc sample)))))) + (_.cover [/.bind] + (n.= (inc mono) + (: (Identity Nat) + (/.bind identity.monad + (|>> inc (:: identity.monad wrap)) + (:: identity.monad wrap mono))))) + (_.cover [/.seq] + (:: (list.equivalence n.equivalence) = + (list@map inc poly) + (|> poly + (list@map (|>> inc (:: identity.monad wrap))) + (: (List (Identity Nat))) + (/.seq identity.monad) + (: (Identity (List Nat)))))) + (_.cover [/.map] + (:: (list.equivalence n.equivalence) = + (list@map inc poly) + (|> poly + (/.map identity.monad (|>> inc (:: identity.monad wrap))) + (: (Identity (List Nat)))))) + (_.cover [/.filter] + (:: (list.equivalence n.equivalence) = + (list.filter n.even? poly) + (|> poly + (/.filter identity.monad (|>> n.even? (:: identity.monad wrap))) + (: (Identity (List Nat)))))) + (_.cover [/.fold] + (n.= (list@fold n.+ 0 poly) + (|> poly + (/.fold identity.monad + (function (_ part whole) + (:: identity.monad wrap + (n.+ part whole))) + 0) + (: (Identity Nat))))) + )))) |