Skip to main content

Sum

inductive Sum[T, U] {
    inl(T)
    inr(U)
}

A value belonging to one of two types.

GitHub

cases​

define cases[V](self, left: T -> V, right: U -> V) -> V {
    sum_cases(self, left, right)
}

Case analysis for this sum value.

inl​

Sum.inl: T -> Sum[T, U]

A value from the left type.

inr​

Sum.inr: U -> Sum[T, U]

A value from the right type.

is_left​

let is_left: Sum[T, U] -> Bool = sum_is_left

True if the value lies on the left side.

is_right​

let is_right: Sum[T, U] -> Bool = sum_is_right

True if the value lies on the right side.

map​

define map[V, W](self, left: T -> V, right: U -> W) -> Sum[V, W] {
    sum_map(self, left, right)
}

Applies maps to both sides.

map_left​

define map_left[V](self, left: T -> V) -> Sum[V, U] {
    sum_map_left(self, left)
}

Applies a map to the left side.

map_right​

define map_right[W](self, right: U -> W) -> Sum[T, W] {
    sum_map_right(self, right)
}

Applies a map to the right side.

match​

Sum.match: (Sum[T*, U*], T* -> R*, U* -> R*) -> R*

swap​

define swap(self) -> Sum[U, T] {
    sum_swap(self)
}

Interchanges the two sides.