*safe* coerce, for regular and existential types

[Ralf Laemmel]

oleg@pobox.com wrote:
> 
> ... loads of cunning stuff omitted 
>

Software-engineering-wise your approach suffers
from an important weakness: a closed world assumption.
The programmer has to maintain your "TI" and pass it
on in all kinds of contexts for the array of types to
be handled. I also had a type-safe and efficient cast
in [1] with a CWA. (I guess it works fine for
extensials.) My CWA was even more serious however.
I use a class for casting whose declaration even
depends on the array of types to be handled. On the
positive side, I didn't need undecidable not even
overlapping instances. Also, the programmer is not
concerned with passing on any type seq like your
"TI". I really admire your use of polymorphic lists
(which are in fact kind of products) to get the
problem of type sequences to the value level. Cool!

Do you see any way to effectively remove this CWA?
(Only then it could serve as a replacement of the
current cast function.) If yes, would you expect that
your approach is more efficient then the one taken in
Data.Typeable? (We recently split up Data.Dynamics
into Data.Dynamics and a more primitive module
Data.Typeable which contains cast; see CVS) Is it obvious
to see that fetching stuff from the type sequences would
be indeed efficient for long PLists? Well, I guess the
hard problem is the CWA anyway.

Ralf

[1] The Sketch of a Polymorphic Symphony
    http://homepages.cwi.nl/~ralf/polymorphic-symphony/
    See the Larghetto movement
    It is trivial; it makes Stephanie Weirich's type-safe
    cast fit for nominal type analysis.


-- 
Ralf Laemmel
VU & CWI, Amsterdam, The Netherlands
http://www.cs.vu.nl/~ralf/
http://www.cwi.nl/~ralf/