CODEWITHSUNDEEP
haskell
jkeuhlen
jkeuhlen

Reputation: 4517

How can you extract type information from a Proxy?

Let's say I have a standard proxy with some type a hidden inside:

pxyA = Proxy :: Proxy a

Because of other parts of my program, I know for a fact that a is actually a tuple of two other types, say (b,c). Is there any way for me to extract that information from my original proxy with a function like: 

f :: Proxy a -> (Proxy b, Proxy c)

or 

f :: Proxy a -> Proxy (b,c)

The main thing stopping me is that I don't know what the types b or c are going to be, just that I need to pass them to other parts of my program.

I've already written a trivial function with a similar form: 

splitPxyTup :: forall a b . Proxy (a,b) -> (Proxy a, Proxy b)
splitPxyTup _ = (Proxy :: Proxy a, Proxy :: Proxy b)

but keep getting lost on how to convince the type system that my original proxy actually is a tuple type.

I also thought about using a cast, but since I don't know what the output types are, I won't be able to get anything meaningful from it.

Upvotes: 2

Views: 399

Answers (2)

luqui
luqui

Reputation: 60513

I've been trying to see what you're after and can't quite, it would be helpful if you could produce a more complete example that represents your problem.

Until then, I seem to have an answer for this part of your question

The main thing stopping me is that I don't know what the types b or c are going to be...

From that sentence it sounds like you need an existential:

proxyTuple :: Proxy a -> exists b c. Proxy (b,c)

which is not valid Haskell, but we can encode it easily:

data ProxyTupleEx where
    ProxyTupleEx :: Proxy (b,c) -> ProxyTupleEx

It's not quite enough though, because we could easily implement this function in a trivial way.

proxyTuple :: Proxy a -> ProxyTupleEx
proxyTuple _ = ProxyTupleEx (Proxy :: Proxy ((), ()))

We need to also specify the connection with the incoming a. This we can do:

data ProxyTupleEx a where
    ProxyTupleEx :: (a ~ (b,c)) => Proxy (b,c) -> ProxyTupleEx a

We won't be able to implement proxyTuple now, because it has no implementation when a is not a tuple. We need

proxyTuple :: Proxy a -> Maybe (ProxyTupleEx a)

giving it the opportunity to fail.

Now we get to your other question about reflection. We need to add a Typeable constraint so that we can reflect about the type, but then it is fairly straightforward once you are used to the cadence of the library:

proxyTuple :: Typeable a => Proxy a -> Maybe (ProxyTupleEx a)
proxyTuple p
    | App _proxy (App (App tuple a) b) <- typeOf p
    , Just HRefl <- eqTypeRep tuple (typeRep :: TypeRep (,))
    = Just (ProxyTupleEx p)
    | otherwise
    = Nothing

Now if you pattern match on a ProxyTupleEx a, the compiler will know that a is actually a tuple.

tupleLength :: (a,b) -> Int
tupleLength _ = 2

example :: Typeable a => Proxy a -> a -> Int
example proxy x
    | Just (ProxyTupleEx _) <- proxyTuple proxy = tupleLength x
                                                  -- x is now known to be a tuple
                                                  -- so this typechecks
    | otherwise = 0

Like magic, this typechecks, and works:

ghci> example Proxy (1,2)
2
ghci> example Proxy 0
0

(Also the Proxy here is unnecessary since we already have the type of a, but I included it for consistency with the query.)

Upvotes: 1

cdk
cdk

Reputation: 6778

This seems easy enough to write, given the limited context available from your question. As long as you can provide a concrete proof of your claim that a ~ (b, c), you just need a bit of Data.Type.Equality machinery to convince GHC.

{-# LANGUAGE GADTs, TypeOperators #-}

import Data.Proxy
import Data.Type.Equality

splitProxyTuple :: a :~: (b, c) -> Proxy a -> Proxy (b, c)
splitProxyTuple Refl = castWith Refl

and using it in a GHCI session

> type T = (Int, Char)
> type F = (Int, Bool)
> let prf = Refl :: (T :~: (Int, Char))
> let prx = Proxy :: Proxy T

> :t splitProxyTuple prf prx
splitProxyTuple prf prx :: Proxy (Int, Char)
=> Proxy

> :t splitProxyTuple prf (Proxy :: Proxy F)
  • Couldn't match type ‘Bool’ with ‘Char’
    Expected type: Proxy T
      Actual type: Proxy F
  • In the second argument of ‘splitProxyTuple’, namely
      ‘(Proxy :: Proxy F)’
    In the expression: splitProxyTuple prf (Proxy :: Proxy F)

Upvotes: 0

Related Questions