Ограничения в пределах RankNTypes

Question

Функция ниже не устанавливает проверку.

test1 :: forall x. (Show x => x) -> String 
test1 = show 

Это потому, что последние -> не имеют доступа к ограничению. (Это, вероятно, не правильная терминология, но, надеюсь, это имеет смысл.) Я пытаюсь найти применение для сигнатур типов, подобных приведенным выше, где окончательный -> не имеет доступа к ограничению. Но я не могу придумать никаких примеров.

Так что мой вопрос: есть ли когда-нибудь случаи, когда нам полезно иметь ограничения в сигнатуре типа, к которой у конечного -> нет доступа?

---

Обратите внимание, что test1 отличается от функции ранга 2 ниже.

test2 :: (forall x. Show x => x) -> String 
test2 = show 

Меня интересует первый случай, а не этот случай. Причина, по которой RankNTypes находится в названии, заключается в том, что это расширение должно быть разрешено для создания сигнатуры типа для test1.

Answer 1

Полезно придумать ограничения класса как аргументы аргументов функции, так как они desugar для функций и функциональных приложений в GHC Core.

Давайте desugar тип в вопросе:

newtype ShowDict a = ShowDict (a -> String) 
test1 :: forall x. (ShowDict x -> x) -> String 

Или еще проще:

test1 :: forall x. ((x -> String) -> x) -> String 

Этот тип не очень полезно. По параметричности его реализации должны быть постоянными функциями, возвращающими некоторую строку.

С оригинальным не-Обессахаренным типом, мы даже не можем сделать что-нибудь с (Show x => x) аргументом, так как нет никакого Show словаря вокруг нашего квантора всеобщности x.

Так что мой вопрос: Есть ли когда-нибудь случай, когда мы это полезно иметь ограничения в сигнатуре типа, что окончательное -> не имеет доступа к ?

Это немного неопределенно сформулировано, но можно утверждать, следующее: типы аргумента функции вида (c x => t) (с x возможно количественно во внешней области видимости) никогда не имеет смысла в Haskell.

Когерентность класса подразумевает, что для каждого типа имеется не более одного экземпляра, поэтому абстрагирование по сравнению с c x не делает никаких вычислительных различий вообще. Если нет c x, тогда функция (desugared) никогда не может быть применена, но если мы уже знаем, что есть уникальный c x, то почему от этого зависит?

Answer 2

Это не значит, что у вас нет доступа к нему, это означает, что экземпляр контроля над типом обращается вспять: используя тип ранга 2, вы меняете того, кто выбирает тип.

В вашем примере функция test2 получает выбор своего аргумента. Так, например, это составляет:

test2 :: (forall x. Show x => x) -> String 
test2 a = show (a :: Char) 

Это происходит потому, что аргумент a должны буквально работать для всех типов, которые являются экземпляром Show. В результате мы никогда не можем позвонить test2, так как мы никогда не сможем предоставить значение, которое может принимать все возможные типы, которые являются экземплярами Show.

Обратите внимание, что если бы мы написали

test2 :: Show x => x -> String 
test2 a = ... 

абонент из test2 получает, чтобы выбрать тип a и test2 является тот, который должен работать для всех экземпляров Show.

Давайте рассмотрим немного более полезный пример:

example :: (forall x. Show x => x -> Int) -> Int 
example f = 10 * f True 

Мы можем видеть, что, опять же, мы (то есть, example) получите, чтобы выбрать тип представленного переменной в x типа (это конкретизирует этот тип переменной относится к определенному типу). Здесь мы выбираем тип Bool. Вот как вы могли бы назвать эту функцию:

ghci> example (length . show) 
40 

Вот еще один пример:

example2 :: (forall x. [x] -> [x]) -> [Int] 
example2 f = f [1, 2, 3] 

Мы можем дать ему какую-либо функции в списках , пока что функция не может заботиться о фактических значениях в том, что список.Поскольку функция не знает тип этих значений, она не может их каким-либо образом проверять (это свойство называется parametricity).

Таким образом, мы можем сделать что-то вроде этого:

ghci> example2 reverse 
[3,2,1] 

... но не что-то вроде этого:

ghci> let addOne :: Int -> Int 
    |>  addOne a = a + 1 
    |> 
ghci> example2 (map addOne) 

<interactive>:33:15: 
    Couldn't match type ‘x’ with ‘Int’ 
     ‘x’ is a rigid type variable bound by 
      a type expected by the context: [x] -> [x] at <interactive>:33:1 
    Expected type: x -> x 
     Actual type: Int -> Int 
    In the first argument of ‘map’, namely ‘addOne’ 
    In the first argument of ‘example2’, namely ‘(map addOne)’ 

Насколько практической полезности идет, ранга п типа используются широко в (например) библиотеку lens. Это позволяет вам выразить мысль о том, что функция использует экземпляр Functor, не зная, какой конкретный экземпляр Functor (то есть он просто использует на нем fmap). Из-за этого, когда вы его передаете, вы можете дать ему любой нужный вам пример Functor.