Почему переменные Haskell не полиморфны, когда связаны сопоставлением с образцом?

Question

Рассмотрим переменную, введенную в шаблон, например, f в этом примере на Haskell:

case (\x -> x) of f -> (f True, f 'c')

Этот код приводит к ошибке типа («Не удалось сопоставить ожидаемый тип« Bool »с фактическим типом« Char »») из-за двух различных вариантов использования f. Это показывает, что предполагаемый тип f не является полиморфным в Haskell.

Но почему бы f не быть полиморфным?

У меня есть две точки сравнения: OCaml и «учебник» Хиндли-Милнера. Оба предполагают, что f должен быть полиморфным.

1. В OCaml аналогичный код не является ошибкой:

   match (fun x -> x) with f -> (f true, f 'c')
   

   Это оценивается как (true, 'c') с типом bool * char. Похоже, что OCaml прекрасно справляется с назначением f полиморфного типа.

2. Мы можем обрести ясность, разобравшись с основами Хиндли-Милнера - лямбда-исчислением с «let», на которых основаны и Haskell, и OCaml. Конечно, применительно к этой базовой системе не существует такой вещи, как сопоставление с образцом. Мы можем провести параллели, хотя. Между «let» и «lambda» case expr1 of f -> expr2 гораздо ближе к let f = expr1 in expr2, чем к (lambda f. expr2) expr1. «Case», как и «let», синтаксически ограничивает привязку f к expr1, тогда как функция lambda f. expr2 не знает, к чему будет привязана f, так как функция не имеет такого ограничения на то, где в программа это будет называться. Это было причиной того, что переменные с ограничением по буквам обобщаются в Хиндли-Милнера, а переменные с привязкой по лямбда - нет. Похоже, что те же самые рассуждения, которые позволяют обобщать переменные с привязкой, показывают, что переменные, введенные сопоставлением с образцом, могут быть обобщены.

Приведенные выше примеры минимальны для ясности, поэтому они показывают только тривиальный шаблон f в сопоставлении с образцом, но все та же логика распространяется на произвольно сложные шаблоны, такие как Just (a:b:(x,y):_), которые могут вводить несколько переменных, которые все будут обобщенная.

Мой анализ верен? В частности, в Haskell - признавая, что это не просто Хиндли-Милнер и не OCaml - почему бы нам не обобщить тип f в первом примере?

Было ли это явным языковым решением, и если да, то каковы были причины? (Я отмечаю, что некоторые в сообществе считают, что даже "let" не следует обобщать , но я бы предположил, что проектное решение предшествует этой статье.)

Если бы переменные, введенные в шаблон, были сделаны полиморфными, похожими на «let», разве это существенно нарушило бы совместимость с другими аспектами Haskell?

Answer 1

Если мы присваиваем полиморфный тип (forall x. t) наблюдателю по делу, то он не соответствует нетривиальному шаблону, поэтому нет смысла иметь case.

Можем ли мы обобщить другим полезным способом? Не совсем, из-за отсутствия поддержки GHC для «непредсказуемой» реализации. В вашем примере Just (a:b:(x,y):_) ни одна связанная переменная не может иметь полиморфный тип, поскольку Maybe, (,) и [] не могут быть созданы с такими типами.

Одна вещь работает, как упомянуто в комментариях: типы данных с полиморфными полями, такими как data Endo = Endo (forall a. a -> a). Однако проверка типов для полиморфных полей технически не включает в себя этап обобщения и не ведет себя как обобщение.

В принципе, обобщение может быть выполнено во многих точках, например, даже при произвольных аргументах функции (например, в f (\x -> x)). Тем не менее, слишком много обобщений засоряет вывод типов, вводя невыполнимые типы более высокого ранга; это также можно понимать как устранение полезных типовых зависимостей между различными частями программы путем удаления нерешенных мета-переменных. Хотя есть системы, которые могут обрабатывать логические операции более высокого ранга гораздо лучше, чем GHC, в особенности MLF , они также намного сложнее и практически не используются. Я лично предпочитаю вообще не иметь молчаливого обобщения.

Answer 2

В дополнение к другим ответам, есть причина того, как переменные типа обрабатываются в сопоставлениях с образцом с точки зрения взаимодействия с экзистенциальными типами. Давайте посмотрим на пару определений из Data.Functor.Coyoneda:

{-# LANGUAGE GADTs #-}

data Coyoneda f a where
    Coyoneda :: (b -> a) -> f b -> Coyoneda f a

lowerCoyoneda :: Functor f => Coyoneda f a -> f a
lowerCoyoneda (Coyoneda g x) = fmap g x

Coyoneda имеет переменную экзистенциального типа, используемую обоими аргументами конструктора. Если GHC не фиксирует этот тип, у fmap in lowerCoyoneda нет способа проверить тип. GHC должен знать, что g и x имеют соответствующие отношения в своих типах, и это требует исправления переменной типа в сопоставлении с образцом.

Answer 3

Первая проблема заключается в том, что с классами типов обобщение не всегда бесплатно. Рассмотрим show :: forall a. Show a => a -> String и это выражение:

case show of
  f -> ...

Если вы обобщите f на f :: forall a. Show a => a -> String, то GHC будет передавать словарь Show при каждом вызове f, а не один раз при единственном вхождении show. В случае нескольких вызовов одного и того же типа это дублирует работу, а не обобщает.

Это также не является обобщением текущего алгоритма вывода типов в сочетании с классами типов: это может привести к тому, что существующие программы больше не будут проверять тип. Например,

    case show of
      f -> f () ++ f mempty

Не обобщая f, мы можем сделать вывод, что mempty имеет тип (). С другой стороны, обобщение f :: forall a. Show a => a -> String потеряет эту связь, и тип mempty в этом выражении будет неоднозначным.

Правда, это незначительные проблемы, и, возможно, с некоторыми мономорфными ограничениями все будет в порядке, даже если они не полностью обратно совместимы.