CODEWITHSUNDEEP
haskellexistential-type
Pier Bezuhoff
Pier Bezuhoff

Reputation: 97

Extracting existential from proxy

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.

Upvotes: 2

Views: 128

Answers (3)

abacabadabacaba
abacabadabacaba

Reputation: 2692

This is not possible. From the documentation:

Proxy is 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.

Upvotes: 1

Alexis King
Alexis King

Reputation: 43852

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.

Upvotes: 8

melpomene
melpomene

Reputation: 85777

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.

Upvotes: 3

Related Questions