Recently entropyfails (http://programmingkungfuqi.blogspot.com/) wrote
to me about the type theoretic formalisation of abstract algebra in Qi.
Abstract algebra studies algebraic structures - objects composed of one
or more sets and a series of operations defined on those sets that
satisfy certain equalities. Our discussion then wandered over to
what a set was in functional progamming terms.
One natural answer is that a set is a non-repeating list of objects.
But what does 'non-repeating' mean here? If we treat the lists within
a 'set' of this kind as potential sets themselves (so [...] is read as
{...}) then our test for set equality has to be invoked on elements of
the compared sets as well as the sets themselves. e.g. [[1 2 3]] is
the same 'set' as [[3 2 1]].
In untyped Qi this test can be simply written. Here it is.
(define equalset?
[X | Y] [W | Z] -> (and (subset? [X | Y] [W | Z]) (subset? [W | Z]
[X | Y]))
X Y -> (= X Y))
(define subset?
[] _ -> true
[X | Y] Z -> (and (member? X Z) (subset? Y Z)))
(define member?
_ [] -> false
X [Y | _] -> true where (equalset? X Y)
X [_ | Z] -> (member? X Z))
Type theoretically testing for the equality of two sets is a tricky
business because the set equality test has to be invoked between the
elements of the two sets. This creates a type clash because the
equality test is operating between objects of type (list A) (the two
lists compared) AND the objects in the lists (of type A). Hence the
native Qi type checker fails the program.
However Qi was designed to compile exotic type theories into code, so
my next thought was "Can we invent a type which would allow us to use
this equality test and also allow us more freedom in the way we
construct our sets?". I decided we could and defined a type operator
rec which was designed to allow lists whose elements could be of the
same type as the lists themsleves. rec has the following properties.
1. [] (the empty list is of type (rec A).
2. If X is of type A then X is of type (rec A).
3. [X | Y] is of type (rec A) iff X is of type (rec A) and Y is of
type (rec A).
Thus a 'set' would be of type (rec number) if it contained either
numbers or sets whose ultimate elements (to use Nelson Goodman's
phrase) are numbers. e.g. [1 [2 3] 4] : (rec number). Here was the
initial shot in Qi.
(datatype rec
X : A;
____
X : (rec A);
________
[] : (rec A);
X : (rec A); Y : (rec A);
==================
[X | Y] : (rec A);)
(define equalset?
{(rec A) --> (rec A) --> boolean}
[X | Y] [W | Z] -> (and (subset? [X | Y] [W | Z]) (subset? [W | Z] [X
| Y]))
X Y -> (= X Y))
(define subset?
{(rec A) --> (rec A) --> boolean}
[] _ -> true
[X | Y] Z -> (and (member? X Z) (subset? Y Z)))
(define member?
{(rec A) --> (rec A) --> boolean}
_ [] -> false
X [Y | _] -> true where (equalset? X Y)
X [_ | Z] -> (member? X Z))
On the first run, this type theory went into an infinite loop; the
culprit being the first rule which looped under unification over types.
(spy +) lets you trace the type checker and it was easy to spot. Qi
allows you to tone down unification to pattern-matching by mode
declarations (see www.lambdassociates.org/FPQi.pdf, page 212 for how to
do this) so I toned it down a bit.
(datatype rec
X : A;
____
X : (mode (rec A) -);
________
[] : (rec A);
X : (rec A); Y : (rec A);
==================
[X | Y] : (rec A);)
On the second run, the program loaded fine.
equalset? : ((rec A) --> ((rec A) --> boolean))
subset? : ((rec A) --> ((rec A) --> boolean))
member? : ((rec A) --> ((rec A) --> boolean))
typechecked in 2296 inferences.
Real time: 0.125 sec.
Run time: 0.109375 sec.
Space: 1378232 Bytes
GC: 2, GC time: 0.03125 sec.
loaded : symbol
The rec type allows you to write a function that extracts Goodman's
'ultimate elements'; the function is, of course, nothing more than the
homely flatten function but closer to its full blooded form as used
within Lisp and other untyped languages than the form generally
encountered in statically typed languages. Haskell and ML users will
no doubt have their own approach.
bw
Mark
"Mark Tarver" <··········@ukonline.co.uk> writes:
> One natural answer is that a set is a non-repeating list of objects.
> But what does 'non-repeating' mean here? If we treat the lists within
> a 'set' of this kind as potential sets themselves (so [...] is read as
> {...}) then our test for set equality has to be invoked on elements of
> the compared sets as well as the sets themselves. e.g. [[1 2 3]] is
> the same 'set' as [[3 2 1]].
This paragraph completely throws me. I look at "a set is a
non-repeating list of objects" and I think "but order
doesn't matter, how is will that be handled" and "But what
does 'non-repeating' mean here?" seems to flag that the
issue is about to be addressed.
However the text talks about invoking the test for set
equality on elements of the compared sets as well as the
sets themselves, as though {{1,2},3} = {1,{2,3}}. Well that
is sounding a bit strange, it would for example break von
Neuman ordinals which have
0 ={}
1 = {{}}
2 = {{},{{}}}
etc.
but then the example is [[1 2 3]] = [[3 2 1]]
which seems to be jumping back to the issue of order not
mattering, so I'm too confused to read on.
Alan Crowe
Edinburgh
Scotland
> This paragraph completely throws me. I look at "a set is a
> non-repeating list of objects" and I think "but order
> doesn't matter, how is will that be handled" and "But what
> does 'non-repeating' mean here?" seems to flag that the
> issue is about to be addressed.
Sorry; perhaps I should fill in that space. Once rec is defined the
following definition of a set will typecheck.
(define set?
{(rec A) --> boolean}
[] -> true
[[X | Y] | Z] -> (and (set? [X | Y]) (and (not (member? [X | Y]
Z)) (set? Z)))
[X | Y] -> (and (not (member? X Y)) (set? Y)))
(6+) (set? [[1 2 3] [3 2 1]])
false : boolean
(7+) (set? [[1 2 3] [3 2 1 4] 5])
true : boolean
(8+) (set? [[1 2 3] [3 2 1 4 4] ])
false : boolean
>
> However the text talks about invoking the test for set
> equality on elements of the compared sets as well as the
> sets themselves, as though {{1,2},3} = {1,{2,3}}. Well that
> is sounding a bit strange, it would for example break von
> Neuman ordinals which have
Not quite certain here of where the problem is.
(10+) (equalset? [[1 2] 3] [1 [2 3]])
false : boolean
Mark