aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/functor/contravariant.lux
blob: 048b34ba812d3188b5d01a7da9d5336e246f6b08 (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
(.module:
  [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)
            ))))