Set interface as a codata type in Polarity (see: https://polarity-lang.github.io)

set.pol

data Bool { T, F }

data Nat { Z, S(n: Nat) }

def (n1: Nat).eq(n2: Nat): Bool {
    Z => n2.match {
        Z => T,
        S(_) => F,
    },
    S(n1) => n2.match {
        Z => F,
        S(n2) => n1.eq(n2),
    },
}

data Eq(a: Type, x y: a) {
    Refl(a: Type, x: a): Eq(a, x, x)
}

// Set interface from Section 3 of “On Understanding Data Abstraction, Revisited”
// by William R. Cook https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf

codata Set { 
    .is_empty: Bool,
    .contains(i: Nat): Bool,
    .insert(i: Nat): Set,
    .union(r: Set): Set,
}

codef Empty: Set {
    .is_empty => T,
    .contains(_) => F,
    .insert(i) => Insert(Empty, i),
    .union(s) => s,
}

#[transparent]
let Insert(s: Set, n: Nat): Set {
    s.contains(n).match {
        T => s,
        F => Insert'(s, n),
    }
}

// NOTE (2025-03-25): Polarity does not currently allow local comatches to use
// self parameters. Instead we lift this to the top-level.
codef Insert'(s: Set, n: Nat): Set {
    .is_empty => F,
    .contains(i) =>
        i.eq(n).match {
            T => T,
            F => s.contains(i),
        },
    .insert(i) => Insert(Insert'(s, n), i),
    .union(r) => Union(Insert'(s, n), r),
}

codef Union(s1 s2: Set): Set {
    .is_empty => F,
    .contains(i) =>
        s1.contains(i).match {
            T => T,
            F => s2.contains(i),
        },
    .insert(i) => Insert(Union(s1, s2), i),
    .union(r) => Union(Union(s1, s2), r),
}

codef Full : Set {
    .is_empty => F,
    .contains(_) => T,
    .insert(_) => Full,
    .union(_) => Full,
}

// Tests

let paper_example : Eq(Bool, Empty.insert(3).union(Empty.insert(1)).insert(5).contains(4), F) {
    Refl(Bool, F)
}

See additional implementations from the paper in OCaml: https://github.com/brendanzab/language-garden/blob/main/scraps/misc-ocaml/set_objects.ml