Lennart Augustsson <[EMAIL PROTECTED]> writes:
> 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.
This sounds good to me; my vaporware language uses a very similar
approach. I'd say your hack is certainly good enough to be better
than not having this feature at all.
> The problem with your <= "magic operator" is that the proof
> is no longer accessible, which I think will make further
> proofs difficult.
Unless you create another "magic" operator to extract the proof...
> -- Lennart
Carl Witty
[EMAIL PROTECTED]
