package preface

  1. Overview
  2. Docs
package preface
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file indexed_monad_plus.ml

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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
module type LAWS_MONOID = sig
  type ('a, 'index) t

  include Indexed_monad.LAWS with type ('a, 'index) t := ('a, 'index) t

  val monad_plus_monoid_1 : unit -> (('a, 'index) t, ('a, 'index) t) Law.t
  val monad_plus_monoid_2 : unit -> (('a, 'index) t, ('a, 'index) t) Law.t

  val monad_plus_monoid_3 :
       unit
    -> ( ('a, 'index) t
       , ('a, 'index) t -> ('a, 'index) t -> ('a, 'index) t )
       Law.t
end

module type LAWS_LEFT_ABSORPTION = sig
  type ('a, 'index) t

  include Indexed_monad.LAWS with type ('a, 'index) t := ('a, 'index) t

  val monad_plus_left_absorb_1 :
    unit -> ('a -> ('b, 'index) t, ('b, 'index) t) Law.t
end

module type LAWS_LEFT_DISTRIBUTIVITY = sig
  type ('a, 'index) t

  include Indexed_monad.LAWS with type ('a, 'index) t := ('a, 'index) t

  val monad_plus_left_distrib_1 :
       unit
    -> ( ('a, 'index) t
       , ('a, 'index) t -> ('a -> ('b, 'index) t) -> ('b, 'index) t )
       Law.t
end

module type LAWS_LEFT_CATCH = sig
  type ('a, 'index) t

  include Indexed_monad.LAWS with type ('a, 'index) t := ('a, 'index) t

  val monad_plus_left_catch_1 :
    unit -> ('a, ('a, 'index) t -> ('a, 'index) t) Law.t
end

module For_monoidal (M : Preface_specs.INDEXED_MONAD_PLUS) :
  LAWS_MONOID with type ('a, 'index) t := ('a, 'index) M.t = struct
  open Law
  include Indexed_monad.For (M)

  let monad_plus_monoid_1 () =
    let lhs = M.(combine neutral)
    and rhs x = x in

    law ("neutral <|> x" =~ lhs) ("x" =~ rhs)
  ;;

  let monad_plus_monoid_2 () =
    let lhs x = M.(combine x neutral)
    and rhs x = x in

    law ("x <|> neutral" =~ lhs) ("x" =~ rhs)
  ;;

  let monad_plus_monoid_3 () =
    let lhs a b c = M.(Infix.(a <|> b) <|> c)
    and rhs a b c = M.(a <|> Infix.(b <|> c)) in

    law ("(a <|> b) <|> c" =~ lhs) ("a <|> (b <|> c)" =~ rhs)
  ;;
end

module For_left_absorption (M : Preface_specs.INDEXED_MONAD_PLUS) :
  LAWS_LEFT_ABSORPTION with type ('a, 'index) t := ('a, 'index) M.t = struct
  include Indexed_monad.For (M)
  open Law

  let monad_plus_left_absorb_1 () =
    let lhs f = M.(neutral >>= f)
    and rhs _ = M.neutral in

    law ("neutral >>= f" =~ lhs) ("neutral" =~ rhs)
  ;;
end

module For_left_distributivity (M : Preface_specs.INDEXED_MONAD_PLUS) :
  LAWS_LEFT_DISTRIBUTIVITY with type ('a, 'index) t := ('a, 'index) M.t = struct
  include Indexed_monad.For (M)
  open Law

  let monad_plus_left_distrib_1 () =
    let lhs a b f = M.(a <|> b >>= f)
    and rhs a b f = M.(a >>= f <|> (b >>= f)) in

    law ("(a <|> b) >>= f" =~ lhs) ("(a >>= f) <|> (b >>= f)" =~ rhs)
  ;;
end

module For_left_catch (M : Preface_specs.INDEXED_MONAD_PLUS) :
  LAWS_LEFT_CATCH with type ('a, 'index) t := ('a, 'index) M.t = struct
  include Indexed_monad.For (M)
  open Law

  let monad_plus_left_catch_1 () =
    let lhs a b = M.(return a <|> b)
    and rhs a _ = M.(return a) in

    law ("(return a) <|> b" =~ lhs) ("return a" =~ rhs)
  ;;
end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct