В Хаскеле, почему eqT, возвращающий Maybe (a: ~: b), работает лучше, чем возвращающий Bool?

Question

Я сделал вариант eqT, который позволил бы мне работать с результатом, как и любой другой Bool, чтобы написать что-то вроде eqT' @a @T1 || eqT' @a @T2.Однако, хотя в некоторых случаях это работало хорошо, я обнаружил, что не могу заменить каждое использование eqT этим.Например, я хотел использовать его, чтобы написать вариант readMaybe, который будет просто Just, когда он должен был вернуть String.Хотя использование eqT позволило мне сохранить тип как String -> Maybe a, использование eqT' требует, чтобы тип был String -> Maybe String.Это почему?Я знаю, что могу сделать это другими способами, но я хочу знать, почему это не работает.Я предполагаю, что это как-то связано со специальной обработкой в ​​случае выражений для GADT (a :~: b является GADT), но что это за специальная обработка?

Вот пример кода, о котором я говорю:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Typeable
import Text.Read

eqT' :: forall a b. (Typeable a, Typeable b) => Bool
eqT' = case eqT @a @b of
    Just Refl -> True
    _ -> False

readMaybeWithBadType1 :: forall a. (Typeable a, Read a) => String -> Maybe String
readMaybeWithBadType1 = if eqT' @a @String
    then Just
    else readMaybe

readMaybeWithBadType2 :: forall a. (Typeable a, Read a) => String -> Maybe String
readMaybeWithBadType2 = case eqT' @a @String of
    True -> Just
    False -> readMaybe

readMaybeWithGoodType :: forall a. (Typeable a, Read a) => String -> Maybe a
readMaybeWithGoodType = case eqT @a @String of
    Just Refl -> Just
    _ -> readMaybe

main :: IO ()
main = return ()

Изменение типа readMaybeWithBadType для возврата Maybe a приводит к жалобам ghc:

u.hs:16:14: error:
    • Couldn't match type ‘a’ with ‘String’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          readMaybeWithBadType1 :: forall a.
                                   (Typeable a, Read a) =>
                                   String -> Maybe a
        at u.hs:14:5-80
      Expected type: String -> Maybe a
        Actual type: a -> Maybe a
    • In the expression: Just
      In the expression: if eqT' @a @String then Just else readMaybe
      In an equation for ‘readMaybeWithBadType1’:
          readMaybeWithBadType1 = if eqT' @a @String then Just else readMaybe
    • Relevant bindings include
        readMaybeWithBadType1 :: String -> Maybe a (bound at u.hs:15:5)
   |
16 |         then Just
   |              ^^^^

u.hs:21:17: error:
    • Couldn't match type ‘a’ with ‘String’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          readMaybeWithBadType2 :: forall a.
                                   (Typeable a, Read a) =>
                                   String -> Maybe a
        at u.hs:19:5-80
      Expected type: String -> Maybe a
        Actual type: a -> Maybe a
    • In the expression: Just
      In a case alternative: True -> Just
      In the expression:
        case eqT' @a @String of
          True -> Just
          False -> readMaybe
    • Relevant bindings include
        readMaybeWithBadType2 :: String -> Maybe a (bound at u.hs:20:5)
   |
21 |         True -> Just
   |                 ^^^^

Я понимаю, почему жалуется, но не вижупочему это не проблема в readMaybeWithGoodType.

Answer 1

По сути, это случай, когда GADT против исключения без GADT.

Когда мы хотим использовать значение x :: T, где T - некоторый алгебраический тип данных, мы прибегаем к сопоставлению с образцом (AKA«исключение»)

case x of
  K1 ... -> e1
  K2 ... -> e2
  ...

, где Ki охватывает все возможные конструкторы.

Иногда вместо использования case мы используем другие формы сопоставления с образцом (например, определение уравнений)но это не имеет значения.Кроме того, if then else полностью эквивалентен case of True -> .. ; False -> ..., поэтому нет необходимости обсуждать это.

Теперь, решающим моментом является то, что тип типа T, который мы исключаем, может быть GADT или нет.

Если это , а не как GADT, тогда все ветви e1,e2,... проверяются по типу, и они должны иметь одинаковый тип.Это делается без использования какой-либо дополнительной информации о типах.

Если мы пишем case eqT' @a @b of ... или if eqT' @a @b then ..., мы исключаем тип Bool, который не является GADT.Никакой информации о a,b не получено с помощью средства проверки типов, и две ветви проверяются на наличие одного типа (который может не работать).

Вместо этого, если T является GADT, средство проверки типа используетдополнительная информация о типе.В частности, если у нас есть case x :: a :~: b of Refl -> e, средство проверки типов узнает a~b и использует это при проверке типов e.

Если у нас есть несколько ветвей, таких как

case x :: a :~: b of
   Just Refl -> e1
   Nothing   -> e2

, тогда a~b используется только для e1, как подсказывает интуиция.

Если вам нужен пользовательский eqT', я предлагаю вам попробовать это:

data Eq a b where
   Equal   :: Eq a a
   Unknown :: Eq a b

eqT' :: forall a b. (Typeable a, Typeable b) => Eq a b
eqT' = case eqT @a @b of
   Just Refl -> Equal
   Nothing   -> Unknown

readMaybe3 :: forall a. (Typeable a, Read a) => String -> Maybe String
readMaybe3 = case eqT' @a @String of
    Equal -> Just
    Unknown -> readMaybe

Хитрость устраняет GADTкоторая предоставляет правильную информацию о переменных типа под рукой, как в этом случае.

Если вы хотите пойти глубже, вы можете проверить языки с полностью зависимыми типами (Coq, Idris, Agda, ...)где мы находим похожее поведение в зависимости от исключения независимой.Эти языки немного сложнее, чем Haskell + GADTs - я должен предупредить вас.Я только добавлю, что зависимое исключение поначалу было для меня загадкой.После того, как я понял общую форму сопоставления с образцом в Coq, все стало иметь смысл.

Answer 2

Благодаря bergey и chi, я думаю, что понимаю последовательность шагов, которые заставили GHC вернуть эту ошибку мне.Они оба являются хорошими ответами, но я думаю, что большая часть моего недопонимания заключалась в том, что я не понимал конкретные шаги, предпринимаемые Haskell для проверки типов, и как это связано, в данном случае, с сопоставлением с шаблоном GADT.Я собираюсь написать ответ, который описывает это в меру моего понимания.

Итак, для начала, одна из вещей, которые делают GADT GADT, состоит в том, что вы можете определить тип суммы, где каждый параметр можетбыть другого типа, который является более конкретным, чем тип, указанный в заголовке объявления данных.Это делает возможным следующее:

data a :~: b where
  Refl :: a :~: a

Так что здесь у нас есть только один конструктор, Refl, который является a :~: b, но более конкретно, этот конкретный конструктор (хотя и единственный) приводит кa :~: a.Если мы составим это с Maybe, чтобы получить тип Maybe (a :~: b), то у нас будет 2 возможных значения: Just Repl :: Maybe (a :~: a) и Nothing :: Maybe (a :~: b).Вот как тип переносит информацию о равенстве типов путем сопоставления с образцом.

Теперь, чтобы заставить GADT работать с сопоставлением с образцом, нужно сделать что-то классное.Дело в том, что выражения, сопоставленные с каждым шаблоном, могут быть более специализированными, чем все выражение соответствия шаблону (например, выражения case).Использование дополнительного уточнения типа, включенного в конструктор GADT, для дальнейшей специализации типа, требуемого для соответствующего выражения, - это специальная обработка, которую Haskell выполняет для GADT при сопоставлении с образцом.Поэтому, когда мы делаем:

readMaybeWithGoodType :: forall a. (Typeable a, Read a) => String -> Maybe a
readMaybeWithGoodType = case eqT @a @String of
    Just Refl -> Just
    _ -> readMaybe

eqT равно Maybe (a :~: b), eqT @a @String, и совпадает _ равно (Typeable a, Read a) => Maybe (a :~: String), но Just Refl равно Maybe (String :~: String).

Haskell потребует, чтобы целое выражение case было расширенным типом (Typeable a, Read a) => String -> Maybe a.Совпадение _, равное readMaybe, имеет тип Read a => String -> Maybe a, который является надмножеством.Тем не менее, Just - это тип a -> Maybe a, который не является надмножеством, потому что выражение case должно включать в себя такие вещи, как String -> Maybe Int, но Just не может вернуть это, потому что это потребуется для String ~ Int.Это то, что происходило при совпадении с Bool.GHC сказал, что он не может соответствовать, Maybe String Just вернется с более общим Read a => Maybe a, который требовался от него.

Это где сопоставление с образцом в конструкторе, который включает эту информацию о равенстве типовэто важно.При сопоставлении с Just Refl :: Maybe (String :~: String) Haskell не нужно, чтобы это совпадающее выражение имело подмножество типа (Typeable a, Read a) => String -> Maybe a, ему просто нужно, чтобы оно было надмножеством String -> Maybe String (подмножество исходного требуемого типа), чтоэто, будучи a -> Maybe a.

Answer 3

Вы обнаружили, что документация описывает как

Чтобы использовать это равенство на практике, сопоставьте шаблон с a: ~: b, чтобы получить конструктор Refl;в теле сопоставления с образцом компилятор знает, что a ~ b.

В большинстве case совпадений на Maybe a, в ветви Just у нас есть дополнительное значение, если типa что мы можем использовать.Здесь также, в Just ветви readMaybeWithGoodType, есть дополнительное значение.Refl не очень интересен на уровне термина, но на уровне типа это так.Здесь он передает GHC факт, который мы знаем путем проверки - что эта ветвь достижима тогда и только тогда, когда a равен String.

Вы правы в том, что другие конструкторы GADT также могут предоставлять информацию о типе (обычновведите ограничения класса (их аргументы) в область видимости.