You're comparing unordered lists of unlimited length with subsets. To define a subset of x, you simply choose whether any element is present or not: type Set

You're comparing unordered lists of unlimited length with subsets. To define a subset of x, you simply choose whether any element is present or not: type Set x = x → Bool Cardinality: 2^x Defining an unordered list (of unlimited length, with possible repetitions) with algebraic data types is harder, if at all possible. Especially when you consider what "unordered" should mean in the face of repetitions. I wouldn't be surprised if it was not possible, or if the expansion turned out to have a strange cardinality such as e^x