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.