Dear Friends of Curry!
Consider the following exercise: In Curry, directed graphs can be
represented as (non-deterministic) successor relation of
type Graph a = a -> a
For example, the graph {(1,2),(1,3),(2,4),(3,4)} can be represented
as operation
succ :: Graph Int
succ 1 = 2; succ 1 = 3; succ 2 = 4; succ 3 = 4
Define operations "undir :: Graph a -> Graph a" and "path :: Graph a -
> a -> a -> [a]" that compute an undirected graph from a directed
one and a path between two given nodes, respectively. One possibility
to solve this exercise is
inv, undir :: Graph a -> Graph a
inv g x | x =:= g y = y where y free
undir g x = g x
undir g x = inv g x
path :: Graph a -> a -> a -> [a]
path g x y | (y:ys) =:= search g [x] = reverse (y:ys) where ys free
search :: Graph a -> [a] -> [a]
search _ xs = xs
search g xs | not (x `elem` xs) = search g (x:xs) where x = g (head
xs) -- no cycles in path
With this definitions, the expression
path (undir succ) 2 3
non-deterministically evaluates to [2,1,3] or [2,4,3] like one would
expect. Many students, however, come up with a slightly different
definition of undir (In a first try, I wrote this myself):
undir g = g
undir g = inv g
With this definition, the expression above has no result rather than
two. Instead of an undirected graph, path is applied to the graph
succ and its inverse non-deterministically due to call-time choice.
The other day, Paco showed us that eta-expansion is incorrect in
presence of non-determinism:
g x = 0
h x = 1
fcoin = g
fcoin = h -- fcoin is a 'functional coin'
The above example differs in that there is nothing a Haskell
programmer would consider a constant, but I admit that it's a minor
difference. My reason to post this example is: I consider it a nice
little program that shows that Curry programmers need to be aware of
the rule Bernd once called the essential property of call-time choice:
f (x?y) = f x ? f y
With this in mind, you soon recognize that
path (undir succ)
should be different from
path (succ ? inv succ)
which is equivalent to
path succ ? path (inv succ)
according to the rule above. I think, only with this rule in mind you
get a clue why the two definitions of undir have different meanings
although they only differ w.r.t. eta-expansion.
I'm looking forward to explaining this to my students ;)
Cheers,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 20 2007 - 08:56:24 CEST