# Set Forms¶

## Syntax¶

setbar := "|" =># "_1";
setbar := "\|" =># "_1";
setbar := "\mid" =># "_1";

setform := spattern ":" stypeexpr setbar sexpr

satom := "{" setform  "}" =># "_2";
satom := "\{" setform  "\}" =># "_2";


## Definition¶

interface set_form[T] { has_elt: T -> bool; }

instance[T] Set[set_form[T], T] {
fun \in (elt:T, s:set_form[T]) => s.has_elt elt;
}

open[T] Set[set_form[T],T];


## Description¶

A set_form is a record type with a single member has_elt which returns true if it’s argument is intended as a member of some particular set.

We construe a set_form as a Set by providing an instance.

A set_form is basically just the membership predicate remodelled as a noun by encapsulating the predicate in a closure and thereby abstracting it.

We provide an inverse image:

fun invimg[t,c2,t2 with Set[c2,t2]]
(f:t->t2, x:c2) : set_form[t] =>
{ e : t | (f e) \in x }
;


## Cartesian Product of set_forms.¶

This uses some advanced instantiation technology to allow you to define the cartesian product of a sequence of sets using the infix TeX operator $$\otimes$$ which is spelled otimes. There’s also a left associative binary operator $$\times$$ spelled times.

## Operators¶

fun \times[U,V] (x:set_form[U],y:set_form[V]) =>
{ u,v : U * V | u \in x and v \in y }
;

fun \otimes[U,V] (x:set_form[U],y:set_form[V]) =>
{ u,v : U * V | u \in x and v \in y }
;

fun \otimes[U,V,W] (head:set_form[U], tail:set_form[V*W]) =>
{ u,v,w : U * V * W | u \in head and (v,w) \in tail }
;

fun \otimes[NH,OH,OT] (head:set_form[NH], tail:set_form[OH**OT]) =>
{ h,,(oh,,ot) : NH ** (OH ** OT) | h \in head and (oh,,ot) \in tail }
;


Example:

var p = \{ x,y: int * int | x == y \};
println\$ (1,1) in p;


# Containers¶

Roughly, a Container is a finite Set. It is a derived type specified in the library with a type class:

class Container [c,v]
{
inherit Set[c,v];
virtual fun len: c -> size;
fun \Vert (x:c) => len x;
virtual fun empty(x: c): bool => len x == size(0);
}


The $$\Vert$$ operator, spelled Vert is an alternative name for len.