safe coerce, for regular and existential types

Sat, 2 Aug 2003 02:21:36 +0800 (GMT-8)

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 oleg@pobox.com 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 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, TypeRep b TI, TypeRep a TI) => a -> m b
> > safeCast a :: m b
> >  = if tr_index a (undefined::TI) == tr_index (undefined::b) (undefined::TI)
> >    then return $ sAFECoerce a
> >    else fail "miscast"
>
> *> *Main> case (EV False) of (EV x) -> (safeCast x)::Maybe Bool
> *> Just False
> *> *Main> case (EV False) of (EV x) -> (safeCast x)::Maybe Int
> *> Nothing
>
> The above examples cast the value of an existentially quantified type
> into a regular type. As we shall see at the end, we can just as well
> cast _into_ an existentially quantified type.
>
> Some of the code in this message is similar to the code posted here
> earlier. However, there are many small and subtle changes. It seemed
> more convenient to include all the code, to make this message
> self-contained.
>
>
> We start with the polymorphic list as a base data structure, as
> before:
>
> > data Nil t r  = Nil
> > data Cons t r = Cons t r
> >
> > class PList ntype vtype cdrtype where
> >     cdr::   ntype vtype cdrtype -> cdrtype
> >     empty:: ntype vtype cdrtype -> Bool
> >     value:: ntype vtype cdrtype -> vtype
> >
> > instance PList Nil vtype cdrtype where
> >     empty = const True
> >
> > instance (PList n v r) => PList Cons v' (n v r) where
> >      empty = const False
> >      value (Cons v r) = v
> >      cdr   (Cons v r) = r
>
>
> We use the polymorphic list to define a finite type map. The map in
> this message has two additional operations: fetch and alter.
>
> > class TypeSeq t s where
> >     type_index:: t -> s -> Int
> >     fetch:: t -> s -> t
> >     alter:: t -> s -> s
> >
> > instance (PList Cons t r) => TypeSeq t (Cons t r) where
> >     type_index _ _ = 0
> >     fetch _ (Cons v _) = v
> >     alter newv (Cons v r)  = Cons newv r
> >
> > instance (PList Cons t' r', TypeSeq t r') => TypeSeq t (Cons t' r') where
> >     type_index v s = 1 + (type_index v $ cdr s)
> >     fetch v s = fetch v $ cdr s
> >     alter newv (Cons v' r') = Cons v' $ alter newv r'
>
> TypeSeq is an associative map between types, values, and integers.
> The operation type_index takes a value and a typemap and returns the
> index of the type of the value in the map. The operation alter takes a
> value and a typemap and returns a new typemap which stores the given
> value. The value can be retrieved either by its index -- or by its
> type. Here we need only the latter: the operation fetch.
>
> We can build the initial typemap
>
> > init_typeseq = Cons (undefined::Char) $
> >                Cons (undefined::Int) $
> > 	         Cons (undefined::Bool) $
> > 	         Cons (undefined::String) $
> > 	         Cons (undefined::Maybe Char) $
> > 	         Nil
>
> We also need the type of init_typeseq, to be used in a type-expression
> context. Alas, there does not seem to be an easy way to take a type of
> a variable in a that context. In the expression context, we can write
> init_typeseq::u and then use the type variable 'u' as needed. In the
> type-expression context (in the context of data and instance
> declarations), this trick does not work. I couldn't find a better
> solution than loading the above definition into GHCi, entering ":t
> init_typeseq" and cutting and pasting GHCi's answer back into the
> code:
>
> > type TI
> >   = Cons
> >     Char
> >     (Cons Int (Cons Bool (Cons String (Cons (Maybe Char) (Nil Bool Bool)))))
>
>
> We can test the typemap as follows
>
> *> *Main> type_index True  init_typeseq
> *> 2
> *> *Main> fetch (undefined::Bool) $ alter True init_typeseq
> *> True
>
> > testmap =
> >   let tp1 = alter True init_typeseq
> >       tp2 = alter 'a' tp1
> >       tp3 = alter False tp2  -- updating the previously-stored value
> >   in (fetch (undefined::Bool) tp3, fetch 'x' tp3)
>
> *> *Main> testmap
> *> (False,'a')
>
> As before, to deal with existentials, we need to extend the above
> compile-time type-mapping to run-time
>
> > class (TypeSeq t u) => TypeRep t u where
> >     tr_index:: t -> u -> Int
> >     tr_index = type_index
> >     inj::  t -> u -> u
> >     inj = alter
> >     prj::  t -> u -> t
> >     prj = fetch
> >
> > instance TypeRep Bool TI
> > instance TypeRep Char TI
> > instance TypeRep String TI
> > instance TypeRep Int TI
>
>
> We can use any TypeSeq -- init_typeseq or any other TypeSeq. We can
> define a number of suitable TypeSeq values in various modules and
> import the most suitable one.
>
> The function sAFECoerce is trivial:
>
> > sAFECoerce a = sAFECoerce' a (init_typeseq::TI)
> >
> > sAFECoerce' (a::a) tenv ::b
> >   = prj (undefined::b) $ inj a tenv
>
> It stores its argument into the type environment, and then retrieves it
> given the target type as the index. If the source and the target types
> are the same, the retrieved value is identical to the argument of
> sAFECoerce'. Otherwise, sAFECoerce' returns whatever value has been
> stored in the typenv under the target type (the default value).
>
>
> We have remarked earlier that this message was intended to solve an
> unstated question in Amr Sabry's original message. The unstated
> question is the need to cast into an existentially quantified
> datatype.  Here's the description of the problem and the stated
> question:
>
> > data F a b =
> >               forall c. (TypeRep c TI) => PushF (a -> c) (F c b)
> >             | Bottom (a -> b)
> >
> > f1 :: Char -> Bool
> > f1 'a' = True
> > f1 _ = False
> >
> > f2 :: Bool -> String
> > f2 True = "true"
> > f2 False = "false"
> >
> > f3 :: String -> Int
> > f3 = length
> >
> > fs = PushF f1 (PushF f2 (PushF f3 (Bottom id)))
>
> ] Is it possible to write a function
> ]   f :: F a b -> T c -> F c b
> ] where (T c) is some type for values of type 'c' or values representing
> ] the type 'c' or whatever is appropriate. Thus if given the
> ] representation of Bool, the function should return:
> ]  PushF f2 (PushF f3 (Bottom id))
> ] and if given the representation of String the function should return
> ]  PushF f3 (Bottom id)
> ] and so on.
>
> The solution given earlier is:
>
> > data HF = forall a b. (TypeRep a TI,TypeRep b TI) => HF (F a b)
> > show_fn_type:: (TypeRep a TI, TypeRep b TI) => (a->b) -> String
> > show_fn_type (g::a->b)
> > 	= "(" ++ (show (tr_index (undefined::a) (undefined::TI) )) ++
> > 	   "->"++(show (tr_index (undefined::b) (undefined::TI))) ++ ")"
> >
> > instance (TypeRep a TI, TypeRep b TI) => Show (F a b) where
> >     show = show . hsf_to_lst . HF
> >        where
> >          hsf_to_lst (HF (Bottom g)) = [show_fn_type g]
> > 	   hsf_to_lst (HF (PushF g next)) = (show_fn_type g):(hsf_to_lst$HF next)
>
> >
> > f':: (TypeRep c TI) => (F a b) -> c -> F a b
> > f' here@(PushF g next::(F a b)) v =
> >     if tr_index v (undefined::TI) == tr_index (g undefined) (undefined::TI)
> >     then here
> >     else case next of
> >           PushF g1 next' -> f' (PushF (g1.g) next') v
> >           Bottom g1      -> f' (Bottom (g1.g)) v
> >
> > f fs v = f' (PushF id fs) v
> >
> > flatten:: (TypeRep a TI, TypeRep b TI) => F a b -> (a -> b)
> > flatten fs :: (a->b)
> >     = case f fs (undefined::b) of
> >         PushF g (Bottom g1) -> g1.g
>
> In short, the function f' takes a data structure F a b and a value of
> type c and returns another data structure F a b, but of a different
> structure
>         PushF g next
> here 'next' has the type F c b -- which is the answer to Amr Sabry's
> question. The function g::a->c is a composition of all previously
> occurring functions. This is a neat "side-effect" of the function f':
> we partially compose the given F a b structure up to the given type.
>
> Technically, the function f' answers Amr Sabry's question. Alas, the
> answer, until now, was useless. The answer, the second field in the
> structure returned by f', is existentially quantified. We can do
> preciously little with it -- until now.
>
> Now we can write
>
> > t1 v = case f fs v of
> >         PushF _ (next::F c b) -> flatten next $ sAFECoerce v
>
> Here we cast into an existential type.
>
> *> *Main> t1 'a'
> *> 4
> *> *Main> t1 False
> *> 5
> *> *Main> t1 "xyz"
> *> 3
>
>
>
> [1] Previous message
> Pure functional TypeRep [Was: Existentials...]
> http://www.haskell.org/pipermail/haskell/2003-July/012330.html
>
> [2] escape from existential quantification
> http://www.haskell.org/pipermail/haskell/2003-February/011288.html
>
> [3] Re: escape from existential quantification
> http://www.haskell.org/pipermail/haskell/2003-February/011293.html
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>

*safe* coerce, for regular and existential types

safe coerce, for regular and existential types