Module Generic_util_sum

module Generic_util_sum: sig .. end

Empty and Sum datatypes.

Types

type empty

Type with zero element.

type ('a, 'b) sum =

`\|`	`Left of 'a`
`\|`	`Right of 'b`

Sum type.

type '_ Ty.t +=

`\|`	`Empty : empty Ty.t`
`\|`	`Sum : 'a Ty.t * 'b Ty.t -> ('a, 'b) sum Ty.t`

Type witnesses for empty and sum.

val left : 'a -> ('a, 'b) sum

val right : 'b -> ('a, 'b) sum

Operations

val empty_elim : empty -> 'a

Empty elimination: anything can be proved from a falsehood. It shouldn't be possible to execute that function since we cannot give it any actual argument, however, the function is useful when pattern matching requires some impossible cases to be given anyway.

val either : ('a -> 'c) -> ('b -> 'c) -> ('a, 'b) sum -> 'c

val sum : ('a -> 'c) ->
       ('b -> 'd) -> ('a, 'b) sum -> ('c, 'd) sum