Is it possible to write extractT?
{-# LANGUAGE ExistentialQuantification #-}
import Data.Proxy
data T = forall t. Show t => T (Proxy t)
extractT :: Proxy T -> T
extractT p = ...
I have tried
extractT p = T $ p >>= \(T t) -> t
but it does not work.
No, it is not possible (aside from “trivial” implementations like this one by melpomene that ignore the argument entirely).
A value of type Proxy a carries no more information at runtime than () does, which is to say it doesn’t carry any information at all. This is true no matter what a is.
Your type T carries more information than just () at runtime: it carries a Show method dictionary for some type around with it. This dictionary isn’t very useful, since by the time the existential is unpacked, you don’t have any way to obtain a value of type t to use show on, but the information is technically there.
Since constructing a T requires supplying a typeclass dictionary, but the dictionary (nor any means to obtain it) does not exist inside Proxy T, and there is not any static information about which type the dictionary should be for, it is impossible to obtain the dictionary necessary to construct a T. Put another way, constructing a value of type Proxy T does not pick a t—there is no type “inside” the T in Proxy T—since Proxy only carries around type-level information, but the t inside the T type only exists at the value level.
extractT :: Proxy T -> T
extractT _ = T (Proxy :: Proxy ())
I'm not sure how useful this is (or how it is "extracting" anything), but it has the required type signature.
This is not possible. From the documentation:
Proxyis a type that holds no data
There is nothing you can extract from a Proxy value besides its type. And the type Proxy T doesn't say anything about the type inside the T value, because there is no T value inside.