Объединяющий c -> a -> b и (a -> b) -> c

Какой тип выводится синтезатором типов на Haskell при объединении типов? c -> a -> b а также (a -> b) -> c?

Может кто-нибудь объяснить мне, как я могу решить это?

Спасибо!

Источник

3 ответа

Решение

Кажется, это какое-то упражнение / домашнее задание, поэтому я не буду все портить, но сначала дам несколько советов:

  • тип c -> a -> b на самом деле c -> (a -> b)
  • так что вы должны объединиться c -> (a -> b) с (a -> b) -> c, то есть:
    • c с a -> b (первая часть)
    • a -> b с c (вторая часть)

теперь, что может (попытаться избавиться от c;)) быть сейчас?

PS: я предполагаю, что вы хотите эти типы a, b.. быть таким же

Источник

В других ответах мы увидели, как выполнить объединение вручную и как спросить ghci некоторые ограниченные вопросы унификации, когда нам не нужно связывать переменные типов в двух типах, которые мы хотим объединить. В этом ответе я покажу, как использовать существующий инструментарий, чтобы ответить на заданный вами вопрос, поскольку, как я понимаю, вы намерены это сделать.

Хитрость заключается в том, чтобы использовать ограничения равенства типов, чтобы попросить GHC объединить два типа, а затем представить результаты как тип кортежа. Ограничение на равенство типов запускает унификатор; когда объединение выполнено, переменные типа в нашем типе кортежа будут упрощены в соответствии с тем, что было изучено во время объединения.

Таким образом, ваш вопрос выглядит так, например:

> :set -XTypeFamilies
> :{
| :t undefined -- a dummy implementation we don't actually care about
| :: ((a -> b) -> c) ~ (c -> a -> b) -- the unification problem
| => (a, b, c) -- how we ask our query (what are the values of a, b, and c after unification?)
| :}
<snip -- a copy of the above text>
  :: (a, b, a -> b)

Из этого мы узнаем, что для любых типов a а также bмы можем выбрать a ~ a, b ~ b, а также c ~ a -> b как решение проблемы объединения. Вот еще один вопрос, который может вас заинтересовать: после объединения какой упрощенный тип (a -> b) -> c? Вы можете запустить предыдущий запрос и заменить в a, b, а также c от руки, или вы могли бы спросить GHCI:

> :t undefined :: ((a -> b) -> c) ~ (c -> a -> b) => (a -> b) -> c
undefined :: ((a -> b) -> c) ~ (c -> a -> b) => (a -> b) -> c
  :: (a -> b) -> a -> b

Единственное, что я изменил в этой команде - это часть запроса. Результат говорит нам, что (a -> b) -> c становится (a -> b) -> a -> b после объединения. Обратите внимание, что a а также b в типе результата не гарантируется, что он точно такой же, как a а также b в запросе - хотя, вероятно, в GHC, это всегда будет так.

Еще один быстрый трюк, который стоит упомянуть, это то, что вы можете использовать Proxy превратить переменную произвольно родственного типа в * тип для использования в кортеже; таким образом, например:

> :t undefined :: f a ~ (b -> c) => (a, b, c, f)

<interactive>:1:42:
    Expecting one more argument to ‘f’
    The fourth argument of a tuple should have kind ‘*’,
      but ‘f’ has kind ‘* -> *’
    In an expression type signature: f a ~ (b -> c) => (a, b, c, f)
    In the expression: undefined :: f a ~ (b -> c) => (a, b, c, f)
> :m + Data.Proxy
> :t undefined :: f a ~ (b -> c) => (a, b, c, Proxy f)
undefined :: f a ~ (b -> c) => (a, b, c, Proxy f)
  :: (c, b, c, Proxy ((->) b))
Источник

Вы можете спросить GHCI

:t [undefined :: c -> a -> b, undefined :: (a -> b) -> c]

Потребуется унифицировать типы, чтобы выяснить, к какому типу относятся элементы списка. Мы можем объединить любое количество типов таким образом; даже 0, попробуйте!

Переменные типа слева в c -> a -> b отличаются от переменных типа справа в a -> b -> c, GHC переименует переменные типа, чтобы сохранить их различимость, но попытается сохранить исходные имена. Это делается путем добавления чисел в конец имен переменных типов. Ответ на этот запрос включает в себя некоторые переменные типа a, a1, b, b1, c, а также c1, Если вы не хотите, чтобы переменные типа были различимы, вы можете прочитать ответ, игнорируя добавленные числа.

Если вы хотите, чтобы переменные типа были различны, может быть немного сложно сказать, что делает GHC, потому что вы не знаете, какие переменные типа были переименованы в какие. В практическом кодировании это может быть проблемой при попытке понять ошибки типа. В обоих случаях есть простое решение: переименуйте переменные типа с отличительными именами самостоятельно, чтобы ghc не нуждался в их переименовании.

:t [undefined :: c1 -> a1 -> b1, undefined :: (a2 -> b2) -> c2]

Мы закончили с тем, что может сделать vanilla Haskell, но вы можете заставить компилятор отвечать на вопросы более широко, используя ограничения равенства типов, как описано в ответе Даниэля Вагнера. Следующий раздел просто описывает почему forall Типы с областями видимости не являются общим решением.

для всех

Прежде чем читать этот раздел, вы должны подумать о том, можно ли объединить, для всехc, c -> a -> b а также (a -> b) -> c,

Опытному хакеллеру может показаться, что вы можете не допустить, чтобы переменные типа отличались друг от друга, введя их в явном виде forall область действия с расширением ScopedTypeVariables. Я не знаю простой способ сделать это в ghci, но следующий фрагмент с дырой† просит компилятор объединить a -> b а также a -> b,

{-# LANGUAGE ScopedTypeVariables #-}

example1 :: forall a b. ()
example1 = (undefined :: _) [undefined :: a -> b, undefined :: a -> b]

Вывод, кажется, говорит нам, что список является списком a -> b,

Found hole `_' with type: [a -> b] -> ()

Если мы попытаемся использовать это в качестве примера проблемы, это не сработает.

example2 :: forall a b c. ()
example2 = (undefined :: _) [undefined :: c -> a -> b, undefined :: (a -> b) -> c]

Компилятор вежливо говорит нам, почему†

Couldn't match type `c' with `a -> b'

Это не правда, что для всех типов c, c это функция. Некоторые примеры типов, которые не являются функциями, включают Int, Bool, а также IO a,

† Я использую (undefined :: _) вместо _ когда спрашиваешь, что это за тип, который входит в лунку. Если вы просто используете _ GHC не проверяет тип все выражения. Компилятор может заставить вас поверить, что дыру можно заполнить, хотя на самом деле это невозможно. На выходе для example2 есть также следующая, крайне вводящая в заблуждение строка

Found hole `_' with type: [c -> a -> b] -> ()
Источник
Другие вопросы по тегам