Re: *safe* coerce, for regular and existential types

2003-08-02 Thread oleg

 Does this technique extend to polymophic types?
Yes, of course. The type F a b in the earlier message was polymorphic.

 Let's say we have the following type:

  data D a = C | D a

 Is it possible to index the type D a?

I have just lifted the polymorphic Maybe -- which is isomorphic to
your type. 
ti maybe_decon (Just True)
ti maybe_decon (Just 'a')
give different results. (ti maybe_decon Nothing) can give either the
same or different indices for different concrete types of
Nothing. It's all up to you. For each new datatype, the user has to
provide two functions: one to deconstruct the datatype into a
polymorphic array of values of already indexable types, and the other
is to re-construct the datatype from the array. As long as the user
can do that -- in _any_ way he wishes -- the mapping is
established. Incidentally, there is no need to add any new type
instances or add new alternatives to datatype declarations. There is
no need to extend the type heap either.

I could post the code but I need to write explanations and perhaps
change a few identifier names to something more meaningful. Alas, it's
already almost 2am, and I want to go home...
Haskell mailing list

Re: *safe* coerce, for regular and existential types

2003-08-01 Thread Ralf Laemmel
 ... 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.


[1] The Sketch of a 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
Haskell mailing list

Re: *safe* coerce, for regular and existential types

2003-08-01 Thread Wang Meng
I admire the elegancy of your code which makes the changes to add new data
types minimum. There is one question I want to ask: Does this technique
extend to polymophic types?

Let's say we have the following type:

 data D a = C | D a

Is it possible to index the type D a? Or there is some fundmental
limitations which make it not achievable by Haskell type classes?

  @ @

On Thu, 31 Jul 2003 [EMAIL PROTECTED] wrote:

 This message describes functions safeCast and sAFECoerce implemented
 in Haskell98 with common, pure extensions. The functions can be used
 to 'escape' from or to existential quantification and to make
 existentially-quantified datatypes far easier to deal with. Unlike
 Dynamic, the present approach is pure, avoids unsafeCoerce and
 unsafePerformIO, and permits arbitrary multiple user-defined typeheaps
 (finite maps from types to integers and values).

 An earlier message [1] introduced finite type maps for
 purely-functional conversion of monomorphic types to unique
 integers. The solution specifically did not rely on Dynamic and
 therefore is free from unsafePerformIO. This message shows that the
 type maps can be used for a safe cast, in particular, for laundering
 existential types. The code in this message does NOT use
 unsafePerformIO or unsafeCoerce. To implement safe casts, we define a
 function sAFECoerce -- which works just like its impure
 counterpart. However the former is pure and safe. sAFECoerce is a
 library function expressed in Haskell with common extension. The
 safety of sAFECoerce is guaranteed by the typechecker itself.

 This whole message is self-contained, and can be loaded as it is in
 GHCi, given the flags
   -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances

 This message was inspired by Amr Sabry's problem on existentials.  In
 fact, it answers an unstated question in Amr Sabry's original message.

 It has been observed on this list that existentially-quantified
 datatypes are not easy to deal with [2]. For example, suppose we have
 a value of a type

  data EV = forall a. (TypeRep a TI)= EV a

 (please disregard the second argument of TypeRep for a moment).

 The constructor EV wraps a value. Suppose we can guess that the
 wrapped value is actually a boolean. Even if our guess is correct, we
 *cannot* pass that value to any function of booleans:

 * *Main case (EV False) of (EV x) - not x
 * interactive:1:
 * Inferred type is less polymorphic than expected
 * Quantified type variable `a' is unified with `Bool'
 * When checking an existential match that binds
 * x :: a
 * and whose type is EV - Bool
 * In a case alternative: (EV x) - not x

 A quantified type variable cannot be unified with any regular type --
 or with another quantified type variable. Values of existentially
 quantified types cannot be passed to monomorphic functions, or to
 constrained polymorphic functions (unless all their constrains have
 been mentioned in the declaration of the existential). That limitation
 guarantees safety -- on the other hand, it significantly limits the
 convenience of existential datatypes [2].

 To overcome the limitation, it _seemed_ that we had to sacrifice
 purity. If we are positive that a particular existentially quantified
 value has a specific type (e.g., Bool), we can use unsafeCoerce to
 cast the value into the type Bool [3]. This approach is one of the
 foundations of the Dynamic library. The other foundation is an ability
 to represent a type as a unique run-time value, provided by the
 methods of the class like TypeRep. Given an existentially quantified
 value and a value of the desired type, Dynamic compares type
 representations of the two values. If they are the same, we can
 confidently use unsafeCoerce to cast the former into the type of the

 This works, yet leaves the feeling of dissatisfaction. For one thing,
 we had to resort to an impure feature. More importantly, we placed our
 trust in something like TypeRep and its members, that they give an
 accurate and unique representation of types. But what if they lie to
 us, due to a subtle bug in their implementation? What if they give the
 same representation for two different types? unsafeCoerce will do its
 dirty work nevertheless. Using the result would lead to grave
 consequences, however.

 This message describes sAFECoerce and the corresponding safe cast.
 Both functions convert the values of one type into the target type.
 One or both of these types may be existentially quantified.  When the
 source and the target types are the same, both functions act as the
 identity function. The safe cast checks that the type representations
 of the source and the target types are the same. If they are, it
 invokes sAFECoerce. Otherwise, we monadically fail. The function
 sAFECoerce does the conversion without any type checking. It always
 returns the value of the target type. If the source type was the same
 as the 

Re: *safe* coerce, for regular and existential types

2003-07-31 Thread Derek Elkins
Throughout this message you imply, if not outright state, that Dynamics
requires unsafeCoerce/unsafePerformIO.  This is simply not the case. 
GHC implements Dynamics with unsafeCoerce, or did last time I checked,
but it can easily be implemented using only existentials. (I presume
that this decision was made either for efficiency, simplicity, and/or
simply that another (readily useable) technique was not known when the
library was made.)

Anyways, as I have often mentioned, A Lightweight Implementation of
Generics and Dynamics has an unsafePerformIO/Coerce free implementation
of Dynamics as well as Generics as the title suggests.

Haskell mailing list