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?
-W-M-
@ @
|
\_/
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
> *>
> *> :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
> latter.
>
> 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 checkin
