Почему эта проверка типов не выполняется в Haskell?

Question

Это не проверка типа:

module DoesntTypeCheck where {
import Prelude(Either(..));
defaultEither :: a -> Either b c -> Either a c;
defaultEither a (Left _) = Left a;
defaultEither _ b = b;
}

Но это делает:

module DoesTypeCheck where {
import Prelude(Either(..));
defaultEither :: a -> Either b c -> Either a c;
defaultEither a (Left _) = Left a;
defaultEither _ (Right b) = Right b;
}

Компилятор, вероятно, глючит, тип Either a c может быть только Left (x::a) илиRight (y::c), если это не Left, то это Right, и мы знаем, что Right :: b -> Either a b так Right (y::c) :: Either a c.

Answer 1

Проблема в том, что когда вы говорите

defaultEither _ b = b

вы говорите, что выходное значение b совпадает со вторым входным значением. И это возможно, только если значения имеют одинаковый тип. Но вы сказали компилятору, что вход имеет тип Either b c, а выход - Either a c. Это разные типы, так что неудивительно, что компилятор жалуется.

Я понимаю, что вы пытаетесь сделать, но даже если значение Right x (с x типа c) само по себе может иметь тип Either d c для любой d вашей подписи типа ограничивает входные и выходные значения версиями с различными d s. А это значит, что вы не можете использовать одну и ту же переменную для ссылки на оба значения.

Answer 2

Давайте попробуем еще более простой пример:

data Foo x = Bar

foobar :: Foo a -> Foo b
foobar f = f

Взгляните на определение Foo. С левой стороны есть переменная типа (x), которая на самом деле нигде не появляется справа. Это пример так называемой «переменной типа фантома». В сигнатуре типа есть тип, который на самом деле не соответствует типу чего-либо в фактическом значении. (И это совершенно законно, кстати.)

Теперь, если у вас есть выражение Just True, то с True :: Bool, тогда Just True :: Maybe True. Однако выражение Nothing определенно является Maybe чем-то . Но при отсутствии фактического значения нет ничего, что могло бы заставить его быть каким-то конкретным типом возможных типов. Переменная типа в данном случае фантомная.

У нас здесь похожая вещь; Bar :: Foo x, для любого x. Так что вы бы подумали , что наше определение foobar является законным.

И вы будете ошибаться .

Нельзя передать значение Foo a, где ожидается значение типа Foo b, , даже если имеют точно такую ​​же структуру времени выполнения. Поскольку средство проверки типов не заботится о структуре времени выполнения; он заботится только о типах . Что касается проверки типов, Foo Int отличается от Foo Bool, хотя во время выполнения нет заметной разницы.

И , что является причиной отклонения вашего кода.

На самом деле, вы должны написать

foobar :: Foo a -> Foo b
foobar Bar = Bar

чтобы средство проверки типов знало, что выводимый вами Bar является новым, отличным Bar от того, который вы получили в качестве ввода (и, следовательно, он может иметь другой тип).

Верьте или нет, это на самом деле функция , а не ошибка. Вы можете написать код, который делает так, чтобы (например) Foo Int вел себя не так, как Foo Char. Хотя во время выполнения они оба просто Bar.

Решение, как вы обнаружили, состоит в том, чтобы просто взять ваше значение b из Right, а затем немедленно вернуть его обратно. Это кажется бессмысленным и глупым, но это должно явно сигнализировать контролеру типов, что типы потенциально изменились. Возможно, это раздражает, но это только один из тех уголков языка. Это не ошибка, он специально разработан для такой работы.

Answer 3

a Любой тип c может быть только ...

Действительно, но в вашем первом примере значение b не имеет типа Either a c! Как показывает ваша сигнатура типа, она имеет тип Either b c. И, конечно, вы не можете вернуть Either b c там, где ожидается Either a c. Вместо этого вы должны деструктурировать значение и восстановить его с правильным типом.

Answer 4

a Любой тип ac может быть только Left (x :: a) или Right (y :: c), если это не Left, то это Right, и мы знаем, что Right :: b -> либо ab, так Справа (y :: c) :: Либо с.

Я думаю, вы путаете type конструкторы с data конструкторами. Either определяется следующим образом: ghc-base:

data  Either a b  =  Left a | Right b

Either - это конструктор type с двумя абстрактными переменными. то есть он принимает любые два типа (Int, String и т. д.). и строит конкретный тип как Either Int String.

Left и Right, с другой стороны, являются data конструкторами. Они принимают фактические значения, такие как 1, "hi" и создают значения, такие как Left 1 и Right "hi".

Prelude> :t Left
Left :: a -> Either a b
Prelude> :t Right
Right :: b -> Either a b

Вывод типа Haskell не не работает с values (Left и Right). Работает только на types (Either). Таким образом, средство проверки типов знает только о Either b c и Either a c - поэтому в первом случае переменные не совпадают.