1

If I've got an v I can call

cast :: a -> Maybe b

So I can take an a and get back a b if the cast is successful (I've elided the details of Typeable constraints).

However, I've got a nastier case. I have a type Value x y. I only actually care about the first type parameter, not the second. So really I want to be able to cast v to Value x y2 and be free in the second parameter (the rest of my code is OK with this).

How can I achieve this? To be clear, at this point I have no idea if v is a Value of any variety, let alone a Value x.

2
  • 3
    That would very much depend on the definition of Value.
    – bheklilr
    Mar 26, 2015 at 22:04
  • 2
    You can't use cast to change types arbitrarily, it will fail. If v :: Value Int Char, then cast v :: Maybe (Value Int Bool) will return Nothing. I think you need a real conversion function, which exploits Value's constructors.
    – chi
    Mar 26, 2015 at 22:21

1 Answer 1

4

cast alone can't do this because it needs to know the types of all variables, but its implementation is quite simple so you can write your own. cast checks a and b are the same type and unsafeCoerces it if they match.

You can do something using typeRepCon. This deconstructs a TypeRep into the type constructer and a list of types that make it's parameters. First match the type constructors to make sure it's a Value, then check if y is the same. If everything matches you can unsafeCoerce.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
import Unsafe.Coerce
import Data.Typeable

data Value x y = Value x y
  deriving Typeable

data Box where
  Box :: Typeable a => a -> Box

value :: Value Int Char
value = Value 3 'a'

box :: Box
box = Box value

box2 :: Box
box2 = Box 'Z'

getValueY :: forall a y. (Typeable a, Typeable y) => a -> Maybe (forall x. Value x y)
getValueY a
  | con == typeRepTyCon (typeOf value) && y == typeRep (Proxy :: Proxy y) 
      = Just $ unsafeCoerce a
  | otherwise = Nothing
  where
    (con, ~[_x, y]) = splitTyConApp (typeOf a)

valueChar :: Value x Char -> Char
valueChar (Value _ c) = c

boxChar :: Box -> Maybe Char
boxChar (Box b) =
  case getValueY b of
    Just v  -> Just (valueChar v)
    Nothing -> Nothing

which gives

>>> getY box
Just 'a'
>>> getY box2
Nothing

The impredicative type (forall x. Value x y) is here to make sure you can't choose what x is, otherwise you could make it whatever you want as long as the y matches. Another (possibly nicer) solution is make another wrapper like

data YValue y where
  YValue :: Value x y -> YValue y
  deriving Typeable

A lot of the trouble comes from not even knowing it's a Value, otherwise you could use gcast.


Edit: you can avoid ImpredicativeTypes completely by giving it a forall x. Value x y -> b function:

withValueY :: forall a y b. (Typeable a, Typeable y)
           => (forall x. Value x y -> b) -> a -> Maybe b
withValueY f a
  | con == typeRepTyCon (typeOf value) && y == typeRep (Proxy :: Proxy y)
      = Just $ f (unsafeCoerce a)
  | otherwise = Nothing
  where
    (con, ~[_x, y]) = splitTyConApp (typeOf a)

boxChar :: Box -> Maybe Char
boxChar (Box b) = withValueY valueChar b
2
  • 2
    This seems like something that would be solved by the proposed Typeable redesign. In particular if the current API had had something like withTypeable, then unsafeCoerce could be avoided because you could construct existentially the desired type to cast into. Or presumably the decomposition functions could be used more directly. Mar 27, 2015 at 0:54
  • I ended up using your second approach and doing forall x y and then using normal casts once I'd asserted in was at least a Value. Mar 27, 2015 at 22:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.