(define $List (lambda [$a] (type {[$var-match (lambda [$tgt] {tgt})] [$inductive-match (deconstructor {[nil [] {[{} {[]}] [_ {}] }] [cons [a (List a)] {[{$x .$xs} {[x xs]}] [_ {}] }] [snoc [a (List a)] {[{.$xs $x} {[x xs]}] [_ {}] }] [join [(List a) (List a)] {[$tgt (let {[$loop (lambda [$ts] (match ts (List a) {[ {[{} {}]}] [ {[{} ts] @(map (lambda [$as $bs] [{x @as} bs]) (loop xs))}]}))]} (loop tgt))] }] [nioj [(List a) (List a)] {[$tgt (let {[$loop (lambda [$ts] (match ts (List a) {[ {[{} {}]}] [ {[{} ts] @(map (lambda [$as $bs] [{@as x} bs]) (loop xs))}]}))]} (loop tgt))] }] })] [$equal? (lambda [$val $tgt] (match [val tgt] [(List a) (List a)] {[[ ] ] [[ ] ] [[_ _] ]}))] }))) (define $map (lambda [$fn $ls] (match ls (List Something) {[ {}] [ {(fn x) @(map fn xs)}]}))) (define $remove (lambda [$a] (lambda [$xs $x] (match xs (List a) {[ {}] [ rs] [ {y @((remove a) rs x)}]})))) (define $remove-all (lambda [$a] (lambda [$xs $x] (match xs (List a) {[ {}] [ ((remove-all a) rs x)] [ {y @((remove-all a) rs x)}]})))) (define $remove-collection (lambda [$a] (lambda [$xs $ys] (match ys (List a) {[ xs] [ ((remove-collection a) ((remove a) xs y) rs)]})))) (define $add (lambda [$a] (lambda [$xs $x] (match ((member? Int) x xs) Bool {[ xs] [ {@xs x}]})))) (define $union (lambda [$a] (lambda [$xs $ys] (match ys (List a) {[ xs] [ ((union a) ((add a) xs y) rs)]})))) (define $subcollections (lambda [$xs] (match xs (List Something) {[ {{}}] [ (let {[$subs (subcollections rs)]} {@subs @(map (lambda [$sub] {x @sub}) subs)})] }))) (define $car (lambda [$xs] (match xs (List Something) {[ x]}))) (define $reverse (lambda [$xs] (match xs (List Something) {[ {}] [ {@(reverse rs) x}]}))) (define $member? (lambda [$a] (lambda [$x $ys] (match ys (List a) {[ ] [ ] [ ((member? a) x ys)] })))) (define $unique (lambda [$a] (lambda [$xs] (let {[$loop (lambda [$xs $ys] (match xs (List a) {[ ys] [ (match ((member? a) x ys) Bool {[ (loop rs ys)] [ (loop rs {@ys x})] [_ {}] })]}))]} (loop xs {}))))) (define $subcollection? (lambda [$a] (lambda [$xs $ys] (match xs (List a) {[ ] [ (match ((member? a) x ys) Bool {[ ] [ ((subcollection? a) rest ys)]})]})))) (define $concat (lambda [$xs] (match xs (List Something) {[ {}] [ {@x @(concat rs)}]}))) (define $Multiset (lambda [$a] (type {[$var-match (lambda [$tgt] {tgt})] [$inductive-match (deconstructor {[nil [] {[{} {[]}] [_ {}] }] [cons [a (Multiset a)] {[$tgt (map (lambda [$t] [t ((remove a) tgt t)]) tgt)] }] [join [(Multiset a) (Multiset a)] {[$tgt (map (lambda [$ts] [ts ((remove-collection a) tgt ts)]) (subcollections tgt))] }] })] [$equal? (lambda [$val $tgt] (match [val tgt] [(Multiset a) (Multiset a)] {[[ ] ] [[ ] ] [[_ _] ]}))] }))) (define $Set (lambda [$a] (type {[$var-match (lambda [$tgt] {tgt})] [$inductive-match (deconstructor {[nil [] {[{} {[]}] [_ {}]}] [cons [a (Set a)] {[$tgt (let {[$tgt2 ((unique a) tgt)]} {@(match-all tgt2 (Multiset a) [ [x xs]]) @(match-all tgt2 (Multiset a) [ [x {@xs x}]])})]}] [join [(Set a) (Set a)] {[$tgt (let {[$tgt2 ((unique a) tgt)]} (concat (map (lambda [$xs $ys] (map (lambda [$sxs] [xs {@ys @sxs}]) (subcollections xs))) (match-all tgt2 (Multiset a) [ [xs ys]]))))]}] })] [$equal? (lambda [$val $tgt] (and ((subcollection? a) val tgt) ((subcollection? a) tgt val)))] })))