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

Question

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

Этот вопрос является дополнением к RankNTypes with type aliases confusion. Проблема там сводилась к типам функций, как этот ...

{-# 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 acannot be moved outside of the type of the second argument (как можно было бы, если бы у нас было 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 - предполагая, что такое происходит на самом деле, что-то, о чем я не уверен. Что же тогда представляет собой точное описание того, что происходит, когда ограничение, похоже, исчезает таким образом?

Answer 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 просто обещает предоставить такой словарь, прежде чем он действительно начнет использовать y, но тогда он не делаетy в любом случае, так что это нормально.

Это в основном так же, как с помощью функции, как это:

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

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

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