(.using
 [library
  [lux (.except)
   ["_" test (.only Test)]
   ["[0]" type]
   [abstract
    [monad (.only do)]]
   [control
    ["[0]" function]]
   [math
    ["[0]" random (.only Random)]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" / (.only Apply)]]
 [//
  [functor (.only Injection Comparison)]])

(def (identity injection comparison (open "/#[0]"))
  (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
  (do [! random.monad]
    [sample (at ! each injection random.nat)]
    (_.property "Identity."
      ((comparison n.=)
       (/#on sample (injection function.identity))
       sample))))

(def (homomorphism injection comparison (open "/#[0]"))
  (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
  (do [! random.monad]
    [sample random.nat
     increase (at ! each n.+ random.nat)]
    (_.property "Homomorphism."
      ((comparison n.=)
       (/#on (injection sample) (injection increase))
       (injection (increase sample))))))

(def (interchange injection comparison (open "/#[0]"))
  (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
  (do [! random.monad]
    [sample random.nat
     increase (at ! each n.+ random.nat)]
    (_.property "Interchange."
      ((comparison n.=)
       (/#on (injection sample) (injection increase))
       (/#on (injection increase) (injection (is (-> (-> Nat Nat) Nat)
                                                 (function (_ f) (f sample)))))))))

(def (composition injection comparison (open "/#[0]"))
  (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
  (type.let [:$/1: (-> Nat Nat)]
    (do [! random.monad]
      [sample random.nat
       increase (is (Random :$/1:)
                    (at ! each n.+ random.nat))
       decrease (is (Random :$/1:)
                    (at ! each n.- random.nat))]
      (_.property "Composition."
        ((comparison n.=)
         (|> (injection (is (-> :$/1: :$/1: :$/1:)
                            function.composite))
             (/#on (injection increase))
             (/#on (injection decrease))
             (/#on (injection sample)))
         (/#on (/#on (injection sample)
                     (injection increase))
               (injection decrease)))))))

(def .public (spec injection comparison apply)
  (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test))
  (_.for [/.Apply]
         (all _.and
              (..identity injection comparison apply)
              (..homomorphism injection comparison apply)
              (..interchange injection comparison apply)
              (..composition injection comparison apply)
              )))