-- choose is the basic non-deterministic choice function
choose x _ = x
choose _ y = y
-- Non-deterministic insertion in a list
insert x [] = [x]
insert x (y:ys) = choose (x:y:ys) (y:insert x ys)
-- Non-deterministic generation of permutations
permut [] = []
permut (x:xs) = insert x (permut xs)
-- In the following definition, 'ys' (i.e. 'permut xs')
-- is lazily generated, as much as the filter 'sorted' demands it.
-- The filter may reject 'ys' without fully constructing it.
sort xs = rId sorted (permut xs)
-- restricted identity: rId p x is x if x satisfies (p x)=True
rId :: (a -> Bool) -> a -> a
rId p x | p x = x
-- this version of sort looks simpler but its behavior is not so
-- clear due to the interpretation of where (sharing or not sharing?)
wheresort xs | sorted ys = ys
where ys = permut xs
strictsort xs | ys =:= permut xs & sorted ys =:= True = ys where ys free
sorted [] = True
sorted [_] = True
sorted (x:y:ys) | x<=y = sorted (y:ys)
goal1 = sort [4,3,2,1]
goal2 = wheresort [4,3,2,1]
goal3 = strictsort [4,3,2,1]
data Nat = o | s Nat
coin = o
coin = s(o)
add o n = n
add (s m) n = s(add m n)
double x = add x x
goal4 = double coin