> ...I thought about this pretty hard. Particularly I thought about using
> classes; this was fruitless. So I decided I'd invent a new language feature
> and a nice little syntax to handle it.
>
> Sorted l r = Ordered r /\ Permutation l r
>
> sort :: (l :: [a]) -> (r :: [a]) <= Sorted l r
You've reinvented subsets. :-)
In more ordinary mathematical notation I'd write
sort :: (l :: [a]) -> { r :: [a] | Sorted l r }
i.e., the range of sort is a subset of the type [a] where
the list is a sorted version of l.
I have also been thinking about how to add this, but I've not
come up with a satisfactory solution yet. This trick is
to make this mesh nicely with type checking.
One solution, admittedly somewhat of a hack, is to be able
to mark one of the components of a record as being the
essential one. E.g.
sort :: (l :: [a]) -> sig { *r :: [a]; s :: Sorted l r }
where the * marks the essential component. The idea being
that if you have something of type `sig { *x :: T; ... }',
but need a `T' you the selection would be implicit. But you
would still be able to access the other components with the
usual . notation. E.g.
let ys = sort l
a = foldr (+) 0 ys -- use it as a list
foo = ys.s -- access the proof
...
I have no idea if this work well in practice or if it is
reasonable to implement. I'm still hoping for a better
idea.
The problem with your <= "magic operator" is that the proof
is no longer accessible, which I think will make further
proofs difficult.
-- Lennart
PS. Have we bored normal Haskell users to tears yet?
