aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/functor/contravariant.lux
blob: 8f379472e70937d580d04c2a5f0bdb7816e6e9e4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [abstract
    [equivalence {"+" Equivalence}]
    [monad {"+" do}]]
   [control
    ["[0]" function]]
   [math
    ["[0]" random]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" / {"+" Functor}]])

(def: (identity equivalence value (open "@//[0]"))
  (All (_ f a) (-> (Equivalence (f a)) (f a) (Functor f) Test))
  (_.test "Law of identity."
          (equivalence
           (@//each function.identity value)
           value)))

(def: .public (spec equivalence value functor)
  (All (_ f a) (-> (Equivalence (f a)) (f a) (Functor f) Test))
  (do random.monad
    [sample random.nat]
    (<| (_.for [/.Functor])
        ($_ _.and
            (..identity equivalence value functor)
            ))))