Re: *safe* coerce, for regular and existential types
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 [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: *safe* coerce, for regular and existential types
[EMAIL PROTECTED] 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/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: *safe* coerce, for regular and existential types
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
*safe* coerce, for regular and existential types
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 target type, the return value has the same bit pattern as the argument. If the types differ, the return value is just some default value of the right type. The user can specify the default value as he wishes. Therefore, we can now write * *Main case (EV False) of (EV x) - not $ sAFECoerce x * True We can also try * *Main case (EV 'a') of (EV x) - not $ sAFECoerce x * *** Exception: Prelude.undefined The default value was 'undefined'. The function safeCast is actually trivial safeCast::(Monad m,
Re: *safe* coerce, for regular and existential types
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 [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
