Ответ 1
Нет, вы не можете этого сделать. Длинным и коротким является то, что вы пытаетесь написать зависимую функцию, и Haskell не является навязчивым языком; вы не можете поднять значение TypeRep до истинного типа, и поэтому нет способа записать тип требуемой функции. Чтобы объяснить это более подробно, я сначала покажу, почему так, как вы сформулировали тип randList, на самом деле не имеет смысла. Затем я объясню, почему вы не можете делать то, что хотите. Наконец, я кратко расскажу о нескольких мыслях о том, что на самом деле делать.
экзистенциалы
Ваша подпись типа для randList не может означать, что вы хотите, чтобы она имела в виду. Помня, что все переменные типа в Haskell универсально оцениваются, он читает
randList :: forall a. Typeable a => [Dynamic] -> IO [a]
Таким образом, я имею право называть его как, скажем, randList dyns :: IO [Int] где угодно; Я должен иметь возможность предоставить возвращаемое значение для всех a, а не просто для некоторого a. Размышляя об этом как о игре, она может выбрать a, а не сама функция. То, что вы хотите сказать (это неверно, синтаксис Haskell, хотя вы можете перевести его в действительный Haskell с помощью экзистенциального типа данных 1), больше похож на
randList :: [Dynamic] -> (exists a. Typeable a => IO [a])
Этот promises, что элементы списка имеют некоторый тип a, который является экземпляром Typeable, но не обязательно каким-либо таким типом. Но даже при этом у вас будут две проблемы. Во-первых, даже если бы вы могли создать такой список, что бы вы могли с ним сделать? И, во-вторых, оказывается, что вы даже не можете его построить.
Поскольку все, что вы знаете об элементах экзистенциального списка, состоит в том, что они являются экземплярами Typeable, что вы можете с ними сделать? Посмотрев на документацию, мы видим, что есть только две функции 2 которые принимают экземпляры Typeable:
-
typeOf :: Typeable a => a -> TypeRep, из самого класса класса (действительно, единственный метод в нем); и -
cast :: (Typeable a, Typeable b) => a -> Maybe b(который реализован с помощьюunsafeCoerceи не может быть написан иначе).
Таким образом, все, что вы знаете о типе элементов в списке, состоит в том, что вы можете называть typeOf и cast на них. Поскольку мы никогда не сможем с пользой сделать что-нибудь еще с ними, наш экзистенциальный способ может быть таким же (опять же, недействительным Haskell)
randList :: [Dynamic] -> IO [(TypeRep, forall b. Typeable b => Maybe b)]
Это то, что мы получаем, если мы применим typeOf и cast к каждому элементу нашего списка, сохраним результаты и выбросим теперь бесполезное экзистенциально типизированное исходное значение. Очевидно, что часть TypeRep этого списка не полезна. И вторая половина списка тоже. Поскольку мы возвращаемся к универсально-квантованному типу, вызывающий объект randList снова имеет право запросить, чтобы они получили Maybe Int, a Maybe Bool или Maybe b для любого (настраиваемого) b по их выбору. (Фактически, они имеют немного больше мощности, чем раньше, поскольку они могут создавать разные элементы списка для разных типов.) Но они не могут понять, из какого типа они преобразуются, если они уже не знают об этом - вы все еще потеряли информацию о типе, которую вы пытались сохранить.
И даже отбросив тот факт, что они не полезны, вы просто не можете создать желаемый экзистенциальный тип здесь. Ошибка возникает при попытке вернуть экзистенциально типизированный список (return $ dynListToList dl). На какой конкретный тип вы звоните dynListToList? Напомним, что dynListToList :: forall a. Typeable a => [Dynamic] -> [a]; таким образом, randList отвечает за сбор, который будет использовать a dynListToList. Но он не знает, какой a выбрать; опять же, что источник вопроса! Таким образом, тип, который вы пытаетесь вернуть, не указан и, следовательно, неоднозначен. 3
Зависимые типы
ОК, так что бы сделать эту экзистенциальную полезную (и возможную)? Ну, у нас есть немного больше информации: мы не только знаем там a, у нас есть TypeRep. Поэтому, возможно, мы сможем упаковать это:
randList :: [Dynamic] -> (exists a. Typeable a => IO (TypeRep,[a]))
Это не совсем хорошо; TypeRep и [a] вообще не связаны. И это именно то, что вы пытаетесь выразить: каким-то образом связать TypeRep и a.
В принципе, ваша цель - написать что-то вроде
toType :: TypeRep -> *
Здесь * - тип всех типов; если вы раньше не видели видов, они должны вводить типы, которые относятся к значениям. * классифицирует типы, * -> * классифицирует конструкторы типа с одним аргументом и т.д. (например, Int :: *, Maybe :: * -> *, Either :: * -> * -> * и Maybe Int :: *.)
С этим вы могли бы написать (еще раз, этот код недействителен Haskell, на самом деле он действительно имеет только мимолетное сходство с Haskell, так как вы не можете его написать или что-то подобное в системе типа Haskell ):
randList :: [Dynamic] -> (exists (tr :: TypeRep).
Typeable (toType tr) => IO (tr, [toType tr]))
randList dl = do
tr <- randItem $ map dynTypeRep dl
return (tr, dynListToList dl :: [toType tr])
-- In fact, in an ideal world, the `:: [toType tr]` signature would be
-- inferable.
Теперь вы обещаете правильную вещь: не то, что существует какой-то тип, который классифицирует элементы списка, но существует некоторый TypeRep, так что его соответствующий тип классифицирует элементы списка. Если бы вы могли это сделать, вы были бы настроены. Но запись toType :: TypeRep -> * в Haskell полностью невозможна: для этого требуется язык, зависящий от языка, поскольку toType tr - это тип, который зависит от значения.
Что это значит? В Haskell это вполне приемлемо для значений, зависящих от других значений; это функция. Значение head "abc", например, зависит от значения "abc". Аналогично, у нас есть конструкторы типов, поэтому допустимо, чтобы типы зависели от других типов; рассмотрим Maybe Int и как это зависит от Int. Мы можем даже иметь значения, зависящие от типов! Рассмотрим id :: a -> a. Это действительно семейство функций: id_Int :: Int -> Int, id_Bool :: Bool -> Bool и т.д. Какое из них зависит от типа a. (Так что действительно, id = \(a :: *) (x :: a) -> x, хотя мы не можем записать это в Haskell, есть языки, где мы можем.)
Тем не менее, у нас никогда не может быть типа, который зависит от значения. Нам может понадобиться такая вещь: представьте Vec 7 Int, тип длин-7 списков целых чисел. Здесь Vec :: Nat -> * -> *: тип, первым аргументом которого должно быть значение типа Nat. Но мы не можем писать такие вещи в Haskell. 4 Языки, которые поддерживают это, называются зависимыми (и мы будем писать id, как мы это делали выше); примеры включают Coq и Agda. (Такие языки часто дублируются как помощники по коррекциям и обычно используются для исследовательской работы, а не для написания реального кода. Зависимые типы сложны, а их полезность для повседневного программирования - это активная область исследований.)
Таким образом, в Haskell мы можем сначала проверить все о наших типах, выбросить всю эту информацию и затем скомпилировать то, что относится только к значениям. Фактически, это именно то, что делает GHC; поскольку мы никогда не можем проверять типы во время выполнения в Haskell, GHC стирает все типы во время компиляции без изменения поведения во время выполнения программы. Вот почему unsafeCoerce легко реализовать (оперативно) и полностью небезопасно: во время выполнения он не работает, но лежит в системе типов. Следовательно, нечто вроде toType полностью невозможно реализовать в системе типа Haskell.
Фактически, как вы заметили, вы даже не можете записать нужный тип и использовать unsafeCoerce. Для некоторых проблем вы можете избежать этого; мы можем записать тип для функции, но только реализуем ее с помощью обмана. Именно так работает fromDynamic. Но, как мы видели выше, нет даже хорошего типа, чтобы дать эту проблему изнутри Haskell. Мнимая функция toType позволяет вам указать тип программы, но вы не можете записать тип toType!
Что теперь?
Итак, вы не можете этого сделать. Что вы должны сделать? Я предполагаю, что ваша общая архитектура не идеальна для Haskell, хотя я ее не видел; Typeable и Dynamic фактически не отображаются в программах Haskell. (Возможно, вы говорите Haskell с акцентом на Python), как говорится.) Если у вас есть только конечный набор типов данных, с которыми вы имеете дело, возможно, вы сможете связать вещи с простым старым алгебраическим типом данных:
data MyType = MTInt Int | MTBool Bool | MTString String
Затем вы можете написать isMTInt и просто использовать filter isMTInt или filter (isSameMTAs randomMT).
Хотя я не знаю, что это такое, вероятно, вы могли бы unsafeCoerce пройти через эту проблему. Но, честно говоря, это не очень хорошая идея, если вы действительно, действительно, действительно, действительно, действительно, действительно знаете, что делаете. И даже тогда, вероятно, нет. Если вам нужно unsafeCoerce, вы узнаете, что это будет не просто удобная вещь.
Я действительно согласен с комментарием Даниэля Вагнера: вы, вероятно, захотите пересмотреть свой подход с нуля. Опять же, поскольку я не видел вашей архитектуры, я не могу сказать, что это будет означать. Может быть, там есть еще один вопрос, если вы можете устранить конкретную трудность.
1 Это выглядит следующим образом:
{-# LANGUAGE ExistentialQuantification #-}
data TypeableList = forall a. Typeable a => TypeableList [a]
randList :: [Dynamic] -> IO TypeableList
Однако, поскольку ни один из этих кодов не компилируется, я думаю, что писать его с помощью exists яснее.
2Технически есть некоторые другие функции, которые выглядят релевантными, например toDyn :: Typeable a => a -> Dynamic и fromDyn :: Typeable a => Dynamic -> a -> a. Тем не менее, Dynamic является более или менее экзистенциальной оболочкой вокруг Typeable s, полагаясь на typeOf и TypeRep, чтобы знать, когда на unsafeCoerce (GHC использует некоторые типы реализации и unsafeCoerce, но вы можете сделайте это, за исключением, возможно, dynApply/dynApp), поэтому toDyn не делает ничего нового. И fromDyn действительно не ожидает своего аргумента типа a; это всего лишь обертка вокруг cast. Эти функции и другие аналогичные функции не обеспечивают дополнительной мощности, недоступной только с помощью typeOf и cast. (Например, возврат к Dynamic не очень полезен для вашей проблемы!)
3 Чтобы увидеть ошибку в действии, вы можете попытаться скомпилировать следующую полную программу Haskell:
{-# LANGUAGE ExistentialQuantification #-}
import Data.Dynamic
import Data.Typeable
import Data.Maybe
randItem :: [a] -> IO a
randItem = return . head -- Good enough for a short and non-compiling example
dynListToList :: Typeable a => [Dynamic] -> [a]
dynListToList = mapMaybe fromDynamic
data TypeableList = forall a. Typeable a => TypeableList [a]
randList :: [Dynamic] -> IO TypeableList
randList dl = do
tr <- randItem $ map dynTypeRep dl
return . TypeableList $ dynListToList dl -- Error! Ambiguous type variable.
Конечно, если вы попытаетесь скомпилировать это, вы получите сообщение об ошибке:
SO12273982.hs:17:27:
Ambiguous type variable `a0' in the constraint:
(Typeable a0) arising from a use of `dynListToList'
Probable fix: add a type signature that fixes these type variable(s)
In the second argument of `($)', namely `dynListToList dl'
In a stmt of a 'do' block: return . TypeableList $ dynListToList dl
In the expression:
do { tr <- randItem $ map dynTypeRep dl;
return . TypeableList $ dynListToList dl }
Но как и вся суть вопроса, вы не можете "добавить сигнатуру типа, которая исправляет эти переменные типа", потому что вы не знаете, какой тип вы хотите.
4 В основном. GHC 7.4 поддерживает подъем типов к видам и для полиморфизма видов; см. раздел 7.8, "Вид полиморфизма и продвижение" , в руководстве пользователя GHC 7.4. Это не приводит к тому, что Haskell будет набираться с наложением - что-то вроде TypeRep -> * пока не выйдет 5 но вы сможете написать Vec с помощью очень выразительных типов, которые выглядят как значения.
5 С технической точки зрения, теперь вы можете записать что-то похожее на желаемый тип: type family ToType :: TypeRep -> *. Однако для этого требуется тип продвигаемого вида TypeRep, а не значение типа TypeRep; и, кроме того, вы все равно не сможете его реализовать. (По крайней мере, я так не думаю, и я не понимаю, как вы это сделаете, но я не специалист в этом.) Но на данный момент мы довольно далеко.