; -*- mode: outline -*-
Bialgebra views.
Remarks and list of errata. Updated: 23 Sep 09
* Sec.3 (onwards) and Fig.3
The non-parametric abstract type |Date| is flimsy. We didn't think up nor
provide its laws in the paper. As its type suggests, |mkDate| is a partial
constructor which would be undefined for bad arguments, for example:
mkDate 31 February (-12)
This explains why in the paper |Date| is only |gsize|'d and not |gmap|'d.
The principle that "every constructable value must be observable" (Sec.4.4,
p.6) holds for the type if undefined values are not considered constructable
(they're not observable).
A better (and typical) example of non-linear ADT is |Data.Complex| which has
a straightforward |Tuple2| view and can be used in generic functions with
the concrete type of pairs |(a,b)|.
Partial-made-total operators are possible:
mkDate :: Date d => Day -> Month -> Year -> Maybe d
getDay :: Date d => d -> Maybe Day
...
but there's no special arrangement for |Maybe| in views.
* Sec.3 and Sec.4
In Sec.4.4 (penultimate paragraph):
"However, an unordered set value cannot be observed, only interrogated
with member (we are referring to unbounded sets as constructed in programs
and assume referential transparency which rules out a non-deterministic
'choice' operator). Extraction can be defined for the former, not the
latter, because unordered sets have no operators |f :: Set a -> a| and |g
:: Set a -> Set a| that let us define |nu = isEmpty /\ f /\ g|. The
definability of |iota| and |epsilon| thus depends on the operators an ADT
provides."
The paper isn't terribly clear about several issues many of which are
epitomised by the previous paragraph.
1. What do we mean by "unordeded" set?
We're referring to an ADT of particular mathematical sets (no order, no
repetitions, element equality) with at least two constructors and one
interrogator:
class Set s where
empty :: Eq a => s a
insert :: Eq a => a -> s a -> s a
member :: Eq a => a -> s a -> Bool
...
The interface should provide operators for union, intersection,
difference, etc, which aren't definable in terms of the previous three.
It's not the case that "every constructable value must be observable".
The only observer is "member". Due to the "unorderedness" property, a set
value does not reflect its history of insertions, hence an insertion
cannot be observed by undoing it.
This explains why the interface does not provide functions:
f :: (Set s, Eq a) => s a -> a
g :: (Set s, Eq a) => s a -> s a
And they cannot be defined in terms of other interface operators. These
observers are needed to observe set values constructed with |empty| and
|insert|. Compare to the ordered-set ADT (Fig.3) where
f = min
g = \s -> remove (min s) s
Consequently, in the context of Sec.4 and reference [24], it's not
possible to define |epsilon| for unordered sets
Another way of looking at it: given the unorderedness of sets, if |f| and
|g| were provided they wouldn't be functions (see point 4 below).
2. What do we mean by "unbounded" set?
Not that it has no upper bound, but that it can grow indefinitely, as long
as there's computer memory. In practice the set will always be finite, but
that's not the issue. We're referring to a way of constructing (and
representing, i.e., dynamic memory) sets. We use "bounded" sets for finite
(completely filled) sets of fixed cardinality or sets whose maximum size
is fixed by the programmer and not by the programming environment
(computer memory, etc).
The set of booleans is a finite set. The set of naturals is an infinite
set.
3. What do we mean by "ordered" set?
In the ADT of ordered sets (Fig.3) we use a Haskell-specific notion of
order, that defined in |class Eq a => Ord a| which defines a *total* order
on top of an equivalence relation.
With partial orders it might not be the case that |iota . epsilon = id|
(Sec.4.4). Take for example an ordered set of sets of integers, ordered by
set inclusion. It has no |Ord| instance. We can't compare {1} and {2}. To
deal with partial orders, in the previous equation |=| means equality up
to permutation of incomparable elements. But this might not generalise.
4. What do we mean by "non-deterministic choice"?
Due to the unorderedness of sets, a choice operator that returns an
element of the set
choice :: (Set s, Eq a) => s a -> a
is not a function, returns different elements when applied to the same
set, hence the non-determinism adjective. That it's not a function follows
from the fact that Leibniz's rule:
s1 = s2 => choice s1 = choice s2
doesn't hold. However, |choice| can be programmed for particular set
implementations as a function. For example, if sets are implemented by
lists without repetitions, |choice| might be implemented by
|head|. However,
s1 = insert 1 (insert 2 empty)
s2 = insert 2 (insert 1 empty)
Sets |s1| and |s2| are equal (as sets) but |choice s1| would deliver 1
whereas |choice s2| would deliver 2. Indeed, |choice| is a function
because there is a canonical representation (lists) inducing an order.
Observers defined in terms of |choice| would be non-deterministic:
remove x s = { y | y in s and y /= choice s } -- not Haskell
remove x s = filterS (/= choice s) s
remove x s = s \ (insert (choice s) empty)
* Sec.6.1 (onwards)
The unhappy |Tuple3| should be renamed to |Triple| or similar.
* Sec.6.1, Fig.5 and Sec.6.3.1 & Fig.7
The |Ord| constraint can be omitted in the |Linear a ListV2| instances.
* Sec.7, p.11, 3rd par., "With regard to efficiency ..."
The complexity measures in this paragraph are wrong. The measures depend on
the complexity of ADT operators and these on the ADT implementation. We
assumed some sort of worse-case scenario (e.g., an implementation of ordered
sets using lists instead of heaps, etc.)
Thus, |gsize| for ordered sets can take O(2n), not O(n^2).
|gmap| for ordered sets can take O(3n), not O(n^2).
The |gmap| for FIFO queues is the one with non-linear complexity. The
elements enqueued are taken from the end of the list so the list is
traversed for each enqueueing