polarity/std/data/list.pol

/// The type of finite lists.
data List(a: Type) {
    /// The canonical empty list.
    Nil(a: Type): List(a),
    /// Appending one element to the front of a list.
    Cons(a: Type, x: a, xs: List(a)): List(a),
}

/// Concatenating two lists together.
def List(a).concat(a: Type, other: List(a)): List(a) {
    Nil(_) => other,
    Cons(_, x, xs) => Cons(a, x, xs.concat(a, other)),
}

/// Appending an element to the end of a list.
def List(a).snoc(a: Type, elem: a): List(a) {
    Nil(_) => Cons(a, elem, Nil(a)),
    Cons(_, x, xs) => Cons(a, x, xs.snoc(a, elem)),
}

/// Reversing the elements of a list.
def List(a).reverse(a: Type): List(a) {
    Nil(_) => Nil(a),
    Cons(_, x, xs) => xs.reverse(a).snoc(a, x),
}