Re: Haskell 2 -- Dependent types?

[Lennart Augustsson]

> Well if the ComplicatedTypeToSpecifySorting is correct (I don't know if
> this is possible, but I suspect it isn't) it will of course not type check.
Of course it is possible.  The types in Cayenne have the same power
as predicate logic, so you can specify most anything you like.

Here's a possible type of sort (again assuming we have some <= available):
[I'm writing this from the top of my head so there might be some
buglets.]

-- sort returns a record with the sorted list and two proofs
sort :: (l :: [a]) -> sig { r :: [a]; o :: Ordered r; p :: Permutation l r }

-- Predicate to test if a list is ordered
Ordered :: [a] -> #
Ordered [] = Truth
Ordered [x] = Truth
Ordered (x:x':xs) = IsTrue (x <= x') /\ Ordered (x':xs)

-- Predicate to test if a list is a permutation of another
Permutation :: [a] -> [a] -> #
Permutation [] [] = Truth
Permutation (x:xs) ys = IsTrue (elem x ys) /\ Permutation xs (ys \\ [x])

IsTrue (True) = Truth
IsTrue (False) = Absurd

data Absurd =                 -- empty type
data Truth = truth            -- one element type
data (/\) a b = (&) a b       -- Conjunction, i.e. pairs

     -- Lennart