Semiquotients #
A data type for semiquotients, which are classically equivalent to
nonempty sets, but are useful for programming; the idea is that
a semiquotient set S
represents some (particular but unknown)
element of S
. This can be used to model nondeterministic functions,
which return something in a range of values (represented by the
predicate S
) but are not completely determined.
- mk' :: (
- )
A member of Semiquot α
is classically a nonempty Set α
,
and in the VM is represented by an element of α
; the relation
between these is that the VM element is required to be a member
of the set s
. The specific element of s
that the VM computes
is hidden by a quotient construction, allowing for the representation
of nondeterministic functions.
Instances For
pure a
is a
reinterpreted as an unspecified element of {a}
.
Instances For
Extract the value from an IsPure
semiquotient.