Извлечение экзистенциала из прокси

Question

Можно ли написать extractT?

{-# LANGUAGE ExistentialQuantification #-}
import Data.Proxy

data T = forall t. Show t => T (Proxy t)

extractT :: Proxy T -> T
extractT p = ...

Я пробовал

extractT p = T $ p >>= \(T t) -> t

, но это не работает.

Answer 1

Нет, это невозможно (кроме «тривиальных» реализаций, таких как , сделанных melpomene , которые полностью игнорируют аргумент).

Значение типа Proxy a не несет большеинформация во время выполнения, чем (), то есть она вообще не несет никакой информации.Это верно независимо от того, что a.

Ваш тип T несет больше информации, чем просто () во время выполнения: он содержит словарь методов Show для некоторого типа.Этот словарь не очень полезен, так как к моменту распаковки экзистенциала у вас нет никакого способа получить значение типа t, чтобы использовать show, но технически информация там есть.

Поскольку построение T требует предоставления словаря классов типов, но словарь (и никакие средства для его получения) не существует внутри Proxy T, и нет никакой статической информации о том, для какого типа должен быть словарь,невозможно получить словарь, необходимый для построения T.Другими словами, построение значения типа Proxy T не выбирает t - нет типа «внутри» T в Proxy T - так как Proxy несет только информацию уровня типа, ноt внутри типа T существует только на уровне значений.

Answer 2

Это невозможно. Из документации :

Proxy - это тип, который не содержит данных

Ничего нельзя извлечь из значения Proxy, кроме его типа. И тип Proxy T ничего не говорит о типе внутри значения T, потому что внутри нет T значения.

Answer 3

extractT :: Proxy T -> T
extractT _ = T (Proxy :: Proxy ())

Я не уверен, насколько это полезно (или как он "извлекает" что-либо), но у него есть требуемая сигнатура типа.