Унификация c → a → b и (a → b) → c

Ответ 1

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

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

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

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

Ответ 2

В других ответах мы видели, как выполнить объединение вручную, и как задать 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))

Ответ 3

Вы можете запросить 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 не являются общим решением.

FORALL

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

Для опытного haskeller может показаться, что вы можете сохранить переменные типа отличными, введя их в явную область forall с помощью ScopedTypeVariables расширение. Я не знаю простого способа сделать это в ghci, но следующий snipet с hole ^† просит компилятор объединить 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] -> ()