Аннотации программного типа в Haskell

Нет, ты не можешь этого сделать. Короче говоря, вы пытаетесь написать функцию с зависимой типизацией, а Haskell не является языком с зависимой типизацией; вы не можете поднять значение TypeRep до истинного типа, поэтому нет возможности записать тип желаемой функции. Чтобы объяснить это более подробно, я сначала покажу, почему то, как вы сформулировали тип randList, на самом деле не имеет смысла. Затем я объясню, почему вы не можете делать то, что хотите. Наконец, я вкратце выскажу пару мыслей о том, что на самом деле делать.

Экзистенциальные

Сигнатура вашего типа для randList не может означать то, что вы хотите. Помня, что все переменные типа в Haskell универсально количественно определены, он читает

randList :: forall a. Typeable a => [Dynamic] -> IO [a]

Таким образом, я имею право называть это, скажем, randList dyns :: IO [Int] где угодно; Я должен иметь возможность предоставить возвращаемое значение для всех a, а не просто для некоторых a. Думая об этом как об игре, в ней вызывающий может выбрать a, а не саму функцию. То, что вы хотите сказать (это недопустимый синтаксис Haskell, хотя вы можете перевести его в действительный Haskell, используя экзистенциальный тип данных ¹), больше похоже на

randList :: [Dynamic] -> (exists a. Typeable a => IO [a])

Это обещает, что элементы списка относятся к некоторому типу a, который является экземпляром Typeable, но не обязательно любым таким типом. Но даже с этим у вас будут две проблемы. Во-первых, даже если бы вы могли составить такой список, что бы вы с ним сделали? А во-вторых, оказывается, что его вообще нельзя даже построить.

Поскольку все, что вы знаете об элементах экзистенциального списка, это то, что они являются экземплярами Typeable, что вы можете с ними сделать? Глядя на документацию, мы видите, что есть только две функции ², которые принимают экземпляры 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, Maybe Bool или Maybe b для любого (типизированного) b по своему выбору. (Фактически, у них немного больше возможностей, чем раньше, поскольку они могут создавать экземпляры разных элементов списка для разных типов.) Но они не могут понять, какой тип они преобразовывают из, если они еще не знайте это - вы все еще потеряли информацию о типе, которую пытались сохранить.

И даже если отбросить тот факт, что они бесполезны, вы просто не можете создать здесь желаемый экзистенциальный тип. Ошибка возникает при попытке вернуть экзистенциально типизированный список (return $ dynListToList dl). На какой конкретный тип вы звоните dynListToList? Напомним, что dynListToList :: forall a. Typeable a => [Dynamic] -> [a]; таким образом, randList отвечает за выбор того, что a dynListToList будет использовать. Но он не знает, какой a выбрать; Опять же, это источник вопроса! Таким образом, тип, который вы пытаетесь вернуть, недооценен и поэтому неоднозначен. ³

Зависимые типы

Хорошо, так что же сделать эту экзистенциальную книгу полезной (и возможной)? Что ж, на самом деле у нас немного больше информации: мы не только знаем, что есть некоторые 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. ⁴ Языки, которые это поддерживают, называются зависимо-типизированными (и позволят нам писать 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, знайте, это не просто удобство.

Я действительно согласен с комментарием Даниэля Вагнера: вы, вероятно, захотите переосмыслить свой подход с нуля. Опять же, поскольку я не видел вашей архитектуры, я не могу сказать, что это будет значить. Возможно, там есть еще один вопрос о переполнении стека, если вы можете выделить конкретную трудность.

¹ Это выглядит следующим образом:

{-# LANGUAGE ExistentialQuantification #-}
data TypeableList = forall a. Typeable a => TypeableList [a]
randList :: [Dynamic] -> IO TypeableList

Однако, поскольку ни один из этих кодов в любом случае не компилируется, я думаю, что написать его с помощью exists будет проще.

² Технически есть некоторые другие функции, которые выглядят актуальными, например _ 83_ и _ 84_. Однако Dynamic является более или менее экзистенциальной оболочкой для Typeables, полагающейся на typeOf и TypeReps, чтобы знать, когда unsafeCoerce (GHC использует некоторые типы, зависящие от реализации и unsafeCoerce, но вы могли бы сделать это таким образом, с возможным исключение _91 _ / _ 92_), поэтому toDyn не делает ничего нового. И fromDyn на самом деле не ожидает своего аргумента типа a; это просто оболочка вокруг cast. Эти и другие подобные функции не предоставляют дополнительных возможностей, которые недоступны только для typeOf и cast. (Например, возврат назад к Dynamic не очень полезен для вашей проблемы!)

{-# 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 }