Я уверен, что все знакомы с общими методами формы:
T DoSomething<T>(T item)
Эта функция также называется параметрически полиморфной (ПП), а именно ПП ранга 1 .
Допустим, этот метод может быть представлен с помощью функционального объекта в форме:
<T> : T -> T
То есть <T>
означает, что он принимает один параметр типа, и T -> T
означает, что он принимает один параметр типа T
и возвращает значение того же типа.
Тогда следующее будет PP-функцией ранга 2:
(<T> : T -> T) -> int
Функция сама не принимает параметры типа, но принимает функцию, которая принимает параметр типа. Вы можете продолжать это итеративно, делая вложение все глубже и глубже, получая ПП все более высокого ранга.
Эта функция действительно редка среди языков программирования. Даже Haskell не позволяет это по умолчанию.
Это полезно? Можно ли описать поведение, которое трудно описать иначе?
Кроме того, что это значит для чего-то быть непредсказуемым ? (в данном контексте)
let sdff = (g : (f : <T> (e : T) => void) => void) => {}
Ответы:
В общем, вы используете полиморфизм более высокого ранга, когда хотите, чтобы вызываемый объект мог выбирать значение параметра типа, а не вызывающего . Например:
Любая функция,
g
которую я передаю этому,f
должна быть в состоянии дать мне значениеInt
from некоторого типа, где единственное, чтоg
известно об этом типе, это то, что он имеет экземплярShow
. Итак, это кошерныеНо это не так:
Одним из особенно полезных приложений является использование определения типов для принудительного определения области значений . Предположим, у нас есть объект типа
Action<T>
, представляющий действие, которое мы можем выполнить для получения результата типаT
, такого как будущее или обратный вызов.Теперь предположим, что у нас также есть объект,
Action
который может распределятьResource<T>
объекты:Мы хотим обеспечить, чтобы эти ресурсы использовались только внутри того места,
Action
где они были созданы, и не использовались совместно различными действиями или разными запусками одного и того же действия, чтобы действия были детерминированными и повторяемыми.Мы можем использовать более высокие-рейтинг типов для достижения этой цели путем добавления параметра
S
кResource
иAction
типов, которая является полностью абстрактно-он представляет собой «область видимости» изAction
. Теперь наши подписи:Теперь , когда мы даем , мы уверены , что , поскольку параметр «сфера» полностью полиморфный, он не может избежать тела -SO любое значения типа , который использует такие , как также не могут уйти!
runAction
Action<S, T>
S
runAction
S
Resource<S, int>
(В Хаскеле это называется
ST
монадой, гдеrunAction
она называетсяrunST
,Resource
называетсяSTRef
иnewResource
называетсяnewSTRef
.)источник
ST
Монада представляет собой очень интересный пример. Можете ли вы привести еще несколько примеров, когда полиморфизм более высокого ранга был бы полезен?data Fetch d = forall a. Fetch (d a) (MVar a)
, которое представляет собой пару запросов к источнику данныхd
и слот для хранения результата. Результат и слот должны иметь совпадающие типы, но этот тип скрыт, поэтому вы можете иметь разнородный список запросов к одному и тому же источнику данных. Теперь вы можете использовать более высокий ранг полиморфизм , чтобы написать функцию , которая извлекает все запросы, данную функцию , которая извлекает один:fetch :: (forall a. d a -> IO a) -> [Fetch d] -> IO ()
.Полиморфизм высшего ранга чрезвычайно полезен. В System F (основной язык типизированных языков FP, с которым вы знакомы), это важно для принятия «типизированных кодировок Церкви», что фактически делает System F программированием. Без них система F совершенно бесполезна.
В системе F мы определяем числа как
Дополнение имеет тип
который является типом более высокого ранга (
forall c.
появляется внутри этих стрелок).Это встречается и в других местах. Например, если вы хотите указать, что вычисление является правильным стилем передачи продолжения (google "codensity haskell"), то вы должны исправить это как
Даже разговор о необитаемом типе в System F требует более высокого ранга полиморфизма
Короче говоря, написание функции в системе чистого типа (System F, CoC) требует более высокого ранга полиморфизма, если мы хотим иметь дело с любыми интересными данными.
В частности, в Системе F эти кодировки должны быть «непредсказуемыми». Это означает, что
forall a.
количественно определяет абсолютно все типы . Это включает в себя тот самый тип, который мы определяем. Вforall a. a
этом наa
самом деле может стоятьforall a. a
снова! В таких языках, как ML, это не так, их называют «предикативными», поскольку переменная типа количественно определяет только набор типов без квантификаторов (называемых монотипами). Наше определениеplus
требуемого impredicativity, а потому , что мы создания экземпляраc
вl : Nat
бытьNat
!Наконец, я хотел бы упомянуть одну последнюю причину, по которой вам нужны как непредсказуемость, так и полиморфизм более высокого ранга даже в языке с произвольно рекурсивными типами (в отличие от System F). В Haskell есть монада для эффектов, называемая «монадой потока состояний». Идея состоит в том, что монада потока состояний позволяет вам мутировать вещи, но требует экранирования, чтобы ваш результат не зависел от чего-либо изменяемого. Это означает, что вычисления ST являются чисто наблюдаемыми. Для выполнения этого требования мы используем полиморфизм более высокого ранга
Здесь, гарантируя, что
a
это ограничено пределами области, в которой мы представляемs
, мы знаем, чтоa
означает хорошо сформированный тип, на который не полагаютсяs
. Мы используемs
для параметризации всех изменяемых вещей в этом конкретном потоке состояний, чтобы мы знали, чтоa
это не зависит от изменяемых вещей и, таким образом, ничто не выходит за рамки этихST
вычислений! Прекрасный пример использования типов для исключения некорректных программ.Кстати, если вы заинтересованы в изучении теории типов, я бы предложил инвестировать в хорошую книгу или две. Трудно выучить этот материал по частям. Я бы предложил одну из книг Пирса или Харпера по теории PL в целом (и некоторые элементы теории типов). Книга "Расширенные темы по типам и языкам программирования" также охватывает большое количество теории типов. Наконец, «Программирование в теории типов Мартина Лофа» является очень хорошим изложением теории интенсиональных типов, изложенной Мартином Лофом.
источник