Цель forall в RankNTypes

Question

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

расширение

{-# LANGUAGE RankNTypes #-} 

multipleOf :: forall a. Integral a => a -> a -> Bool 
multipleOf divisor n = n `mod` divisor == 0 

Этот язык является новым для меня, но, как я понимаю, это совпадает с простым:

multipleOf :: Integral a => a -> a -> Bool 
multipleOf divisor n = n `mod` divisor == 0 

Каждый пример ранга типов N I» что вы, кажется, не добавили ничего нового в полиморфизм, который уже был доступен, и этот синтаксис forall, похоже, не добавляет никакого значения.

Что мне не хватает? Есть ли хороший пример того, что этот синтаксис forall выходит за рамки доступных без расширений?

Answer 1

Вы упускаете, что вы можете ограничить область переменной количественному типа:

modifyPair :: (Num b, Num c) => (forall a. Num a => a -> a) -> (b, c) -> (b, c) 
modifyPair f (b, c) = (f b, f c) 

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

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

Существует дополнительный трюк, который вы можете выполнить с помощью этой оснастки. Канонический пример исходит от ST. Цель библиотеки ST - разрешить ограниченное использование изменяемых данных. То есть вы можете реализовать алгоритм, включающий истинную мутацию, и представить внешний интерфейс, который является чистым. ST сами заботятся доказательства того, что использование безопасно с помощью уловок системы умного типа:

newtype ST s a = ... -- details aren't important 
newtype STRef s a = ... -- details still aren't important 

-- a standard-ish interface to mutable data 
newSTRef :: ST s (STRef s a) 
readSTRef :: STRef s a -> ST s a 
writeSTRef :: STRef s a -> a -> ST s() 

-- the magic using RankNTypes 
runST :: (forall s. ST s a) -> a 

Это дополнительный типа переменного, s, стоит обратить внимание. Он отображается как в ST, так и в STRef. Каждая функция, которая управляет STRef, гарантирует, что s в ST и STRef является той же переменной. Поэтому, когда вы доберетесь до runST, вы обнаружите, что тип s не имеет отношения к типу a. s имеет более ограниченную область, чем у a. Конечным результатом этого является то, что вы не можете написать что-то вроде runST newSTRef. Средство проверки типов отклонит его, потому что переменная типа s должна будет избежать контекста, в котором она определена.

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