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
*
* 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
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 checking. It always
returns the value of the target type. If the source type was the same
as the
