aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/functor/contravariant.lux
blob: 9e50001c5f360665773c856aaf38c688eb6bc9a6 (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
     ["." function]]
    [math
     ["." random]
     [number
      ["n" nat]]]]]
  [\\library
   ["." / (#+ Functor)]])

(def: (identity equivalence value (^open "@//."))
  (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)
            ))))