Go backward to Sum Domains Go up to Top Go forward to Function Domains

Sum Domains

Finite lists

Domain D^* = Unit + D + (D x D)
    + (D x (D x D)) + ...
Operations

nil: D^*
nil = inUnit()
cons: D x D^* -> D^*
cons(d,l) =
    cases l of
        isUnit() -> inD(d)
        isD(y) -> inDxD(d,y)
        isDxD(y) -> inDx(DxD)(d,y)
        ...
    end
hd: D^* -> D hd(l) =
    cases l of
        isUnit() -> error
        isD(y) -> y
        isDxD(y) -> fst(y)
        isDx(DxD)(y) -> fst(y)
        ...
    end