Какова цель Rank2Types?

Ответ 1

Не работают ли в Haskell функции полиморфных аргументов?

Они делают, но только из ранга 1. Это означает, что, хотя вы можете написать функцию, которая принимает разные типы аргументов без этого расширения, вы не можете написать функцию, которая использует свой аргумент как разные типы в одном вызове.

Например, следующая функция не может быть введена без этого расширения, поскольку g используется с разными типами аргументов в определении f:

f g = g 1 + g "lala"

Обратите внимание, что вполне возможно передать полиморфную функцию в качестве аргумента другой функции. Так что что-то вроде map id ["a","b","c"] совершенно законно. Но функция может использовать ее только как мономорфную. В примере map используется id, как если бы он имел тип String -> String. И, конечно же, вы можете передать простую мономорфную функцию данного типа вместо id. Без rank2types нет возможности для функции требовать, чтобы ее аргумент был полиморфной функцией и, следовательно, также не мог использовать ее в качестве полиморфной функции.

Ответ 2

Трудно понять полиморфизм более высокого ранга, если вы не изучаете System F напрямую, потому что Haskell предназначен, чтобы скрыть детали от вас в интерес простоты.

Но в основном, основная идея состоит в том, что у полиморфных типов действительно нет формы a -> b, которую они делают в Haskell; в действительности они выглядят так, всегда с явными кванторами:

id :: ∀a.a → a
id = Λt.λx:t.x

Если вы не знаете символ "∀", он читается как "для всех"; ∀x.dog(x) означает "для всех x, x - собака". "Λ" - это капитал лямбда, используемый для абстрагирования по параметрам типа; что вторая строка говорит о том, что id - это функция, которая принимает тип t, а затем возвращает функцию, параметризованную этим типом.

Вы видите, что в System F вы можете просто сразу же применить функцию типа id к значению; сначала вам необходимо применить Λ-функцию к типу, чтобы получить λ-функцию, которую вы применяете к значению. Так, например:

(Λt.λx:t.x) Int 5 = (λx:Int.x) 5
                  = 5

Standard Haskell (т.е. Haskell 98 и 2010) упрощает это для вас, не имея ни одного из этих кванторов типа, капитальных приложений лямбда и типа, но за кулисами GHC помещает их, когда анализирует программу для компиляции. (Я думаю, что это все время компиляции, без накладных расходов во время выполнения.)

Но автоматическая обработка Haskell означает, что он предполагает, что "∀" никогда не появляется в левой ветки типа функции ( "→" ). Rank2Types и RankNTypes отключите эти ограничения и разрешите переопределять правила по умолчанию для Haskell, где можно вставить forall.

Зачем вам это нужно? Потому что полная, неограниченная система F - хелла мощная, и она может делать много классных вещей. Например, тип сокрытия и модульность могут быть реализованы с использованием типов более высокого ранга. Возьмем, к примеру, простую старую функцию следующего типа ранга-1 (чтобы установить сцену):

f :: ∀r.∀a.((a → r) → a → r) → r

Чтобы использовать f, сначала вызывающий должен выбрать, какие типы использовать для r и a, а затем предоставить аргумент полученного типа. Таким образом, вы можете выбрать r = Int и a = String:

f Int String :: ((String → Int) → String → Int) → Int

Но теперь сравните это со следующим типом более высокого ранга:

f' :: ∀r.(∀a.(a → r) → a → r) → r

Как работает функция этого типа? Ну, чтобы использовать его, сначала укажите, какой тип использовать для r. Скажем, мы выбираем Int:

f' Int :: (∀a.(a → Int) → a → Int) → Int

Но теперь ∀a находится внутри стрелки функции, поэтому вы не можете выбрать, какой тип использовать для a; вы должны применить f' Int к Λ-функции соответствующего типа. Это означает, что реализация f' позволяет выбрать, какой тип использовать для a, а не для вызывающего абонента f'. Без типов более высокого ранга, напротив, вызывающий всегда выбирает типы.

Для чего это полезно? Ну, для многих вещей на самом деле, но одна идея заключается в том, что вы можете использовать это для моделирования таких вещей, как объектно-ориентированное программирование, где "объекты" связывают некоторые скрытые данные вместе с некоторыми методами, которые работают с скрытыми данными. Так, например, объект с двумя методами: один, который возвращает Int, а другой, который возвращает String, может быть реализован с помощью этого типа:

myObject :: ∀r.(∀a.(a → Int, a -> String) → a → r) → r

Как это работает? Объект реализуется как функция, которая имеет некоторые внутренние данные скрытого типа a. Чтобы фактически использовать объект, его клиенты передают функцию "обратного вызова", которую объект будет вызывать с помощью двух методов. Например:

myObject String (Λa. λ(length, name):(a → Int, a → String). λobjData:a. name objData)

Здесь мы, в основном, вызываем второй метод объекта, тип которого a → String для неизвестного a. Ну, неизвестно клиентам myObject; но эти клиенты знают, из подписи, что они смогут применить к ним одну из двух функций и получить либо Int, либо String.

Для фактического примера Haskell ниже приведен код, который я написал, когда я учил себя RankNTypes. Это реализует тип под названием ShowBox, который связывает значение некоторого скрытого типа вместе со своим экземпляром класса Show. Обратите внимание, что в нижнем примере я делаю список ShowBox, первый элемент которого был сделан из числа, а второй - из строки. Поскольку типы скрыты с использованием типов более высокого ранга, это не нарушает проверку типов.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

type ShowBox = forall b. (forall a. Show a => a -> b) -> b

mkShowBox :: Show a => a -> ShowBox
mkShowBox x = \k -> k x

-- | This is the key function for using a 'ShowBox'.  You pass in
-- a function @[email protected] that will be applied to the contents of the 
-- ShowBox.  But you don't pick the type of @[email protected] argument--the 
-- ShowBox does.  However, it restricted to picking a type that
-- implements @[email protected], so you know that whatever type it picks, you
-- can use the 'show' function.
runShowBox :: forall b. (forall a. Show a => a -> b) -> ShowBox -> b
-- Expanded type:
--
--     runShowBox 
--         :: forall b. (forall a. Show a => a -> b) 
--                   -> (forall b. (forall a. Show a => a -> b) -> b)
--                   -> b
--
runShowBox k box = box k


example :: [ShowBox] 
-- example :: [ShowBox] expands to this:
--
--     example :: [forall b. (forall a. Show a => a -> b) -> b]
--
-- Without the annotation the compiler infers the following, which
-- breaks in the definition of 'result' below:
--
--     example :: forall b. [(forall a. Show a => a -> b) -> b]
--
example = [mkShowBox 5, mkShowBox "foo"]

result :: [String]
result = map (runShowBox show) example

PS: для всех, кто читает это, кто задавался вопросом, почему ExistentialTypes в GHC использует forall, я считаю, что причина в том, что он использует эту технику за кулисами.

Ответ 3

Ответ Луиса Касильяса дает много отличной информации о том, что означают типы 2-го уровня, но я просто разберусь с одной точки, которую он не покрыл. Требование полиморфизма аргумента не только позволяет использовать его с несколькими типами; он также ограничивает то, что эта функция может делать со своими аргументами (аргументами) и как она может произвести свой результат. То есть, это дает абоненту меньшую гибкость. Почему вы хотите это сделать? Я начну с простого примера:

Предположим, что у нас есть тип данных

data Country = BigEnemy | MediumEnemy | PunyEnemy | TradePartner | Ally | BestAlly

и мы хотим написать функцию

f g = launchMissilesAt $ g [BigEnemy, MediumEnemy, PunyEnemy]

который принимает функцию, которая должна выбрать один из элементов списка, который она задала, и вернуть ракеты запуска IO для этой цели. Мы могли бы дать f простой тип:

f :: ([Country] -> Country) -> IO ()

Проблема в том, что мы могли случайно запустить

f (\_ -> BestAlly)

и тогда у нас будут большие неприятности! Предоставление f полиморфного типа ранга 1

f :: ([a] -> a) -> IO ()

не помогает вообще, потому что мы выбираем тип a, когда вызываем f, и мы просто специализируем его на Country и снова используем наш вредоносный \_ -> BestAlly. Решением является использование типа ранга 2:

f :: (forall a . [a] -> a) -> IO ()

Теперь функция, которую мы передаем, должна быть полиморфной, поэтому \_ -> BestAlly не будет вводить проверку! Фактически, никакая функция, возвращающая элемент, который не указан в списке, будет иметь тип typecheck (хотя некоторые функции, которые попадают в бесконечные циклы или создают ошибки и, следовательно, никогда не возвращаются, будут делать это).

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

Ответ 4

Типы более высокого ранга не так экзотичны, как выяснили другие ответы. Верьте или нет, многие объектно-ориентированные языки (включая Java и С#!) Показывают их. (Конечно, никто в этих сообществах не знает их пугающим названием "типы более высокого ранга".)

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

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

interface IEmployeeVisitor<T>
{
    T Visit(PermanentEmployee e);
    T Visit(Contractor c);
}

class XmlVisitor : IEmployeeVisitor<string> { /* ... */ }
class PaymentCalculator : IEmployeeVisitor<int> { /* ... */ }

Дело в том, что многие посетители с разными типами возвращаемых данных могут работать с одними и теми же данными. Это означает, что IEmployee не должно выражать никакого мнения относительно того, что должно быть T.

interface IEmployee
{
    T Accept<T>(IEmployeeVisitor<T> v);
}
class PermanentEmployee : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}
class Contractor : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}

Я хочу обратить ваше внимание на типы. Обратите внимание, что IEmployeeVisitor универсально количественно определяет возвращаемый тип, тогда как IEmployee определяет его внутри своего метода Accept, т.е. Более высокого ранга. Неоднозначно переводится с С# на Haskell:

data IEmployeeVisitor r = IEmployeeVisitor {
    visitPermanent :: PermanentEmployee -> r,
    visitContractor :: Contractor -> r
}

newtype IEmployee = IEmployee {
    accept :: forall r. IEmployeeVisitor r -> r
}

Итак, у вас это есть. Типы более высокого ранга отображаются в С# при написании типов, содержащих общие методы.

Ответ 5

Слайды из курса Брайана О'Салливана Хаскелла в Стэнфорде помогли мне понять Rank2Types.

Ответ 6

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

например. в TypeScript вы можете написать:

type WithId<T> = T & { id: number }
type Identifier = <T>(obj: T) => WithId<T>
type Identify = <TObj>(obj: TObj, f: Identifier) => WithId<TObj>

Посмотрите, как общий тип функции Identify требует общую функцию типа Identifier? Это делает функцию Identify более высокой.