Can't properly define transformation from universal type, that defined with GADT

Question

I've defined an universal data type that can contain anything (well, with current implementation not totally anything)!

Here it is (complete code):

{-#LANGUAGE NoMonomorphismRestriction#-}
{-#LANGUAGE GADTs#-}
{-#LANGUAGE StandaloneDeriving#-}

data AnyT where
    Any :: (Show a, Read a) => a -> AnyT

readAnyT :: (Read a, Show a) => (String -> a) -> String -> AnyT
readAnyT readFun str = Any $ readFun str

showAnyT :: AnyT -> String
showAnyT (Any thing) = show thing

deriving instance Show AnyT --Just for convinience!

a = [Any "Hahaha", Any 123]

And I can play with it in console:

*Main> a
[Any "Hahaha",Any 123]
it :: [AnyT]
*Main> readAnyT (read::String->Float) "134"
Any 134.0
it :: AnyT
*Main> showAnyT $ Any 125
"125"
it :: String

---

Well, I have it, but I need to process it somehow. For example, let's define transformation functions (functions definition, add to previous code):

toAnyT :: (Show a, Read a) => a -> AnyT -- Rather useless
toAnyT a = Any a

fromAny :: AnyT -> a
fromAny (Any thing) = thing

And there is the problem! the fromAny definition from previous code is incorrect! And I don't know how to make it correct. I get the error in GHCi:

2.hs:18:23:
    Could not deduce (a ~ a1)
    from the context (Show a1, Read a1)
      bound by a pattern with constructor
                 Any :: forall a. (Show a, Read a) => a -> AnyT,
               in an equation for `fromAny'
      at 2.hs:18:10-18
      `a' is a rigid type variable bound by
          the type signature for fromAny :: AnyT -> a at 2.hs:17:12
      `a1' is a rigid type variable bound by
           a pattern with constructor
             Any :: forall a. (Show a, Read a) => a -> AnyT,
           in an equation for `fromAny'
           at 2.hs:18:10
    In the expression: thing
    In an equation for `fromAny': fromAny (Any thing) = thing
Failed, modules loaded: none.

I tried some other ways that giving errors too.

---

I have rather bad solution for this: defining necessary functions via showAnyT and read (replace previous function definitions):

toAnyT :: (Show a, Read a) => a -> AnyT -- Rather useless
toAnyT a = Any a

fromAny :: Read a => AnyT -> a
fromAny thing = read (showAnyT thing)

Yes, it's work. I can play with it:

*Main> fromAny $ Any 1352 ::Float
1352.0
it :: Float
*Main> fromAny $ Any 1352 ::Int
1352
it :: Int
*Main> fromAny $ Any "Haha" ::String
"Haha"
it :: String

But I think it's bad, because it uses string to transform.

Could you please help me to find neat and good solution?

Answer 1

First a disclaimer: I don't know the whole context of the problem you are trying to solve, but the first impression I get is that this kind of use of existentials is the wrong tool for the job and you might be trying to implement some code pattern that is common in object-oriented languaged but a poor fit for Haskell.

That said, existential types like the one you have here are usually like black holes where once you put something in, the type information is lost forever and you can't cast the value back to its original type. However, you can operate on existential values via typeclasses (as you've done with Show and Read) so you can use the typeclass Typeable to retain the original type information:

import Data.Typeable

data AnyT where
    Any :: (Show a, Read a, Typeable a) => a -> AnyT

Now you can implement all the functions you have, as long as you add the new constraint to them as well:

readAnyT :: (Read a, Show a, Typeable a) => (String -> a) -> String -> AnyT
readAnyT readFun str = Any $ readFun str

showAnyT :: AnyT -> String
showAnyT (Any thing) = show thing

toAnyT :: (Show a, Read a, Typeable a) => a -> AnyT -- Rather useless
toAnyT a = Any a

fromAny can be implemented as returning a Maybe a (since you cannot be sure if the value you are getting out is of the type you are expecting).

fromAny :: Typeable a => AnyT -> Maybe a
fromAny (Any thing) = cast thing

Answer 2

You're using GADTs to create an existential data type. The type a in the constructor existed, but there's no way to recover it. The only information available to you is that it has Show and Read instances. The exact type is forgotten, because that's what your constructor's type instructs the type system to do. "Make sure this type has the proper instances, then forget what it is."

There is one function you've missed, by the way:

readLike :: String -> AnyT -> AnyT
readLike s (Any a) = Any $ read s `asTypeOf` a

Within the context of the pattern match, the compiler knows that whatever type a has, there is a Read instance, and it can apply that instance. Even though it's not sure what type a is. But all it can do with it is either show it, or read strings as the same type as it.

Answer 3

What you have is something called Existential type. If you follow that link than you will find that in this pattern the only way to work with the "data" inside the container type is to use type classes.

In your current example you mentioned that a should have Read and Show instances and that means only the functions in these type classes can be used on a and nothing else and if you want to support some more operations on a then it should be constrained with the required type class.

Think it like this: You can put anything in a box. Now when you extract something out of that box you have no way to specify what you will get out of it as you can put anything inside it. Now if you say that you can put any eatable inside this box, then you are sure that when you pick something from this box it will be eatable.