Re: Haskell 2 -- Dependent types?

[Martin Norb{ck]

Sat Feb 20 1999, Nick Kallen ->
: >   sort :: (l :: [a]) -> ComplicatedTypeToSpecifySorting l
: >
: > Well, here's an implementation:
: >
: >   sort xs = sort xs
: >
: > It's type correct, but doesn't really do what you want.
: 
: What if you do this:
: 
: sort (x:xs) = sort elts_lt_x ++ sort elts_greq_x
:                  where
:                    elts_lt_x   = [y | y <- xs, y < x]
:                    elts_greq_x = [y | y <- xs, y >= x]
: 
: (i.e., you leave out the pivot [x])
: 
: Obviously the result of sort will no longer be a permutation of its
: argument. Will this then not type check?

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.
The sort function always returns the empty list or bottom.

        n.

-- 
--[ www.dtek.chalmers.se/~d95mback ]---[ PGP: 0x453504F1 ]---[ UIN: 4439498 ]--