Случай исчезающего ограничения: странности типа более высокого ранга

Все эксперименты, описанные ниже, были выполнены с помощью GHC 8.0.1.

Этот вопрос является продолжением RankNTypes с путаницей типов псевдонимов. Проблема там сводилась к типам функций, подобных этой...

{-# LANGUAGE RankNTypes #-}

sleight1 :: a -> (Num a => [a]) -> a
sleight1 x (y:_) = x + y

... которые отклоняются с помощью проверки типа...

ThinAir.hs:4:13: error:
    * No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            sleight1 :: a -> (Num a => [a]) -> a
    * In the pattern: y : _
      In an equation for `sleight1': sleight1 x (y : _) = x + y

... потому что ограничение более высокого ранга Num a не может быть перемещено за пределами типа второго аргумента (что было бы возможно, если бы мы имели a -> a -> (Num a => [a]) вместо). Таким образом, мы в конечном итоге пытаемся добавить ограничение более высокого ранга на переменную, уже определенную по всему предмету, то есть:

sleight1 :: forall a. a -> (Num a => [a]) -> a

При этом повторении мы можем попытаться немного упростить пример. Позвольте заменить (+) на то, что не требует Num, и разобрать тип проблемного аргумента от типа результата:

sleight2 :: a -> (Num b => b) -> a
sleight2 x y = const x y

Это не работает так же, как и раньше (за исключением незначительных изменений в сообщении об ошибке):

ThinAir.hs:7:24: error:
    * No instance for (Num b) arising from a use of `y'
      Possible fix:
        add (Num b) to the context of
          the type signature for:
            sleight2 :: a -> (Num b => b) -> a
    * In the second argument of `const', namely `y'
      In the expression: const x y
      In an equation for `sleight2': sleight2 x y = const x y
Failed, modules loaded: none.

Использование const здесь, однако, возможно, не является необходимым, поэтому мы могли бы сами попытаться написать реализацию:

sleight3 :: a -> (Num b => b) -> a
sleight3 x y = x

Удивительно, но это действительно работает!

Prelude> :r
[1 of 1] Compiling Main             ( ThinAir.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t sleight3
sleight3 :: a -> (Num b => b) -> a
*Main> sleight3 1 2
1

Еще более странно, по-видимому, нет фактического ограничения Num для второго аргумента:

*Main> sleight3 1 "wat"
1

Я не совсем уверен, как сделать это понятным. Возможно, мы могли бы сказать, что, так же, как мы можем жонглировать undefined, пока мы никогда не оцениваем его, неудовлетворительное ограничение может прилипать к типу, просто прекрасному, если оно не используется для объединения нигде в правой части. Это, однако, похоже на довольно слабую аналогию, специально учитывая, что не строгость, как мы обычно понимаем, это понятие, включающее ценности, а не типы. Более того, это не делает нас ближе к пониманию того, как в мире String объединяется с Num b => b - если предположить, что такое происходит на самом деле, то, о чем я не уверен. Что же тогда представляет собой точное описание того, что происходит, когда ограничение, похоже, исчезает таким образом?

Ответы

Ответ 1

О, он становится еще более странным:

Prelude> sleight3 1 ("wat"+"man")
1
Prelude Data.Void> sleight3 1 (37 :: Void)
1

См., существует фактическое ограничение Num для этого аргумента. Только потому, что (как уже прокомментировал ци), b находится в ковариантной позиции, это не ограничение, которое вы должны предоставить при вызове sleight3. Скорее всего, вы можете выбрать любой тип b, то что бы это ни было, sleight3 предоставит для него экземпляр Num!

Ну, ясно, что фиктивный. sleight3 не может предоставить такой экземпляр num для строк, и определенно не для Void. Но на самом деле это также не нужно, потому что, как вы сказали, аргумент, для которого это ограничение применяется, никогда не оценивается. Напомним, что ограниченно-полиморфное значение по существу является просто функцией словарного аргумента. sleight3 просто promises, чтобы предоставить такой словарь, прежде чем он действительно сможет использовать y, но тогда он не использует y каким-либо образом, так что это нормально.

Это в основном то же самое, что и с такой функцией:

defiant :: (Void -> Int) -> String
defiant f = "Haha"

Опять же, функция аргумента явно не может дать Int, потому что для ее оценки не существует значения Void. Но это тоже не нужно, потому что f просто игнорируется!

В отличие от этого, sleight2 x y = const x y делает sorta use y: второй аргумент const является просто типом ранга-0, поэтому компилятору необходимо разрешить любые необходимые словари в этой точке. Даже если const в конечном счете также выбрасывает y, он все еще "заставляет" достаточно этого значения, чтобы было очевидно, что он не хорошо напечатан.