6.4.22. Линейные типы

LinearTypes

Подразумевает:: MonoLocalBinds
Начиная с версии:: 9.0.1
Статус:: Экспериментальный

Включает линейную стрелку a %1 -> b и стрелку с полиморфизмом по кратности a %m -> b.

Это расширение пока считается экспериментальным: ожидайте ошибки, недочёты и неудачные сообщения об ошибках; всё, вплоть до синтаксиса, может измениться. В частности, см. Ограничения ниже. Мы призываем вас экспериментировать с этим расширением и сообщать о проблемах в трекере ошибок GHC, добавляя тег LinearTypes.

Функция f является линейной, если при условии, что её результат используется ровно один раз, её аргумент также используется ровно один раз. Интуитивно это означает, что в каждой ветви определения f её аргумент x должен использоваться ровно один раз. Это можно сделать, например, так:

Вернуть x без изменений.
Передать x линейной функции и использовать результат ровно один раз тем же способом.
Сопоставить с образцом x и использовать каждый аргумент ровно один раз тем же способом.
Вызвать его как функцию и использовать результат ровно один раз тем же способом.

С помощью -XLinearTypes можно написать f :: a %1 -> b, чтобы обозначить, что f — линейная функция из a в b. Если включено UnicodeSyntax, стрелку %1 -> можно записать как ⊸.

Чтобы единообразно обрабатывать линейные функции a %1 -> b и функции без ограничений a -> b, введён новый тип функции a %m -> b. Здесь m — тип нового рода Multiplicity. Имеем:

data Multiplicity = One | Many  -- Defined in GHC.Types

type a %1 -> b = a %One  -> b
type a  -> b = a %Many -> b

(См. Повышение типов данных.)

Переменную, ограничение кратности которой равно Many, называют неограниченной.

Стрелка с полиморфизмом по кратности a %m -> b также доступна в префиксной форме GHC.Exts.FUN m a b, которую можно применять частично. Однако см. Ограничения.

Линейные стрелки и стрелки с полиморфизмом по кратности всегда объявляются, а не выводятся. Иными словами, если не задать для функции подходящую сигнатуру типа, для неё будет выведен тип обычной функции a -> b. Тот же принцип применяется к полиморфизму представления (см. Вывод и выбор типа по умолчанию).

6.4.22.1. Выражения

При определении функции как лямбда-выражения \x -> u или с помощью уравнений f x = u кратность переменной x выводится из контекста. Для уравнений контекстом обычно служит сигнатура типа. Например, вот линейная функция:

f :: (a -> b) %1 -> a -> b
f g x = g x

В этом примере g должна использоваться линейно, тогда как x не ограничена.

6.4.22.1.1. Связывания

Связывания let и where также могут быть линейными; кратность связываний обычно выводится.

f :: A %1 -> B
g :: B %1 -> C

h :: A %1 -> C
h x = g y
  where
    y = f x

Если вы не хотите или не можете полагаться на вывод, связывания let и where можно аннотировать кратностью.

f :: A %1 -> B
g :: B %1 -> C

h :: A %1 -> C
h x = g y
  where
    %1 y = f x

Точные правила таковы: связывание можно аннотировать кратностью, если:

Связывание не является глобальным
Связывание нерекурсивное
Связывание является связыванием с образцом (включая простую переменную) p=e (нельзя написать let %1 f x = u; вместо этого напишите let %1 f = \x -> u)
Либо p является строгим (см. раздел Строгие образцы ниже), либо p является переменной. В частности, ни x@y, ни (x) не считаются «переменной»

Если аннотация кратности отсутствует, кратность выводится следующим образом:

Для глобальных связываний выводится кратность Many
Для рекурсивных связываний выводится кратность Many
Для ленивых связываний с образцом, не являющимся переменной, выводится кратность Many (обратите внимание: в связываниях let и where образцы по умолчанию ленивые, поэтому let (x,y) = rhs всегда имеют кратность Many, тогда как let !(x,y) = rhs могут иметь кратность 1).
Во всех остальных случаях, включая связывания функций let f x1...xn = rhs, кратность выводится из терма.

Если -XMonoLocalBinds отключено, верно также следующее:

Связывания с образцом, не являющимся переменной, и аннотацией кратности (например, let %1 !(x,y) = rhs) никогда не обобщаются.
Для связываний с образцом, не являющимся переменной, которые выводятся как полиморфные или квалифицированные, выводится кратность Many.

6.4.22.1.2. Строгие образцы

GHC считает, что ленивые образцы, не являющиеся переменными, потребляют проверяемое значение с кратностью Many. На практике образец является строгим (и, следовательно, может быть линейным), если выполняется одно из условий (в противном случае образец ленивый):

Образец является альтернативой case и не аннотирован ~
Образец является связыванием let и аннотирован !
Образец является связыванием let, включено Strict, и образец не аннотирован ~
Образец вложен в строгий образец

Вот несколько примеров влияния на линейную типизацию:

Без -XStrict:

-- good
let %1 x = u in …

-- good
let %1 !x = u in …

-- bad
let %1 (x, y) = u in …

-- good
let %Many (x, y) = u in …

-- good
let %1 !(x, y) = u in …

-- good
let %1 (!(x, y)) = u in …

-- inferred unrestricted
let (x, y) = u in …

-- can be inferred linear
case u of (x, y) -> …

-- inferred unrestricted
case u of ~(x, y) -> …

С -XStrict:

-- good
let %1 x = u in …

-- good
let %1 !x = u in …

-- good
let %1 (x, y) = u in …

-- bad
let %1 ~(x, y) = u in …

-- good
let %Many ~(x, y) = u in …

-- can be inferred linear
let (x, y) = u in …

-- inferred unrestricted
let ~(x, y) = u in …

6.4.22.2. Типы данных

По умолчанию все поля в алгебраических типах данных линейны (даже если -XLinearTypes не включено). Для следующего объявления:

data T1 a = MkT1 a

значение MkT1 x можно конструировать и деконструировать в линейном контексте:

construct :: a %1 -> T1 a
construct x = MkT1 x

deconstruct :: T1 a %1 -> a
deconstruct (MkT1 x) = x  -- must consume `x` exactly once

При использовании в качестве значения MkT1 получает тип с полиморфизмом по кратности: MkT1 :: forall {m} a. a %m -> T1 a. Благодаря этому MkT1 можно использовать в функциях высшего порядка. Дополнительный аргумент кратности m помечен как выводимый (см. Выводимые и заданные переменные типа), поэтому он не конфликтует с явным применением типа. При отображении типов, если не включено -XLinearTypes, функции с полиморфизмом по кратности печатаются как обычные функции (см. Вывод типов с полиморфизмом по кратности); поэтому конструкторы выглядят как функции обычного типа.

mkList :: [a] -> [T1 a]
mkList xs = map MkT1 xs

Следовательно, линейность конструкторов типов незаметна, если -XLinearTypes отключено.

Линейность поля конструктора данных можно настраивать с помощью синтаксиса GADT или синтаксиса записей. Для следующего объявления:

data T2 a b c where
    MkT2 :: a -> b %1 -> c %1 -> T2 a b c -- Note unrestricted arrow in the first argument

значение MkT2 x y z можно сконструировать, только если x не ограничено. С другой стороны, линейная функция, сопоставляющая с образцом MkT2 x y z, должна использовать y и z ровно один раз, но для x ограничений нет. Тот же пример можно записать с помощью синтаксиса записей:

data T2 a b c = MkT2 { x %'Many :: a, y :: b, z :: c }

И снова конструктор MkT2 имеет тип MkT2 :: a -> b %1 -> c %1 -> T2 a b c. Обратите внимание: по умолчанию поля записей линейны; аннотация кратности нужна только для неограниченных полей. Аннотация не влияет на селекторы записей. Поэтому x имеет тип x :: T2 a b c -> a, а y, соответственно, имеет тип y :: T2 a b c -> b.

Также можно определить поле с полиморфизмом по кратности:

data T3 a m where
    MkT3 :: a %m -> T3 a m

или использовать синтаксис записей:

data T3 a m = MkT3 { x %m :: a }

Линейные поля обобщаются (MkT1 :: forall {m} a. a %m -> T1 a в предыдущем примере), а поля с полиморфизмом по кратности — нет; невозможно напрямую использовать MkT3 как функцию a -> T3 a One.

Если LinearTypes отключено, все поля считаются линейными, включая поля GADT, определённые со стрелкой ->.

В объявлении newtype поле должно быть линейным. Попытка записать неограниченный конструктор newtype с помощью синтаксиса GADT приводит к ошибке.

6.4.22.3. Вывод типов с полиморфизмом по кратности

Если LinearTypes отключено, при выводе переменным кратности в типах по умолчанию присваивается Many, как описано в разделе Вывод типов с полиморфизмом представления. Иными словами, без LinearTypes функции с полиморфизмом по кратности a %m -> b выводятся как обычные функции Haskell2010 a -> b. Это позволяет обобщать существующие библиотеки для линейных типов с сохранением обратной совместимости; общие типы видны только в том случае, если пользователь включил LinearTypes. (Обратите внимание: библиотека может объявить линейную функцию в контравариантной позиции, то есть принимать линейную функцию в качестве аргумента. В этом случае линейность нельзя скрыть: она является существенной частью открытого интерфейса.)

6.4.22.4. Ограничения

Линейные типы всё ещё считаются экспериментальными и имеют ряд ограничений. Если вы ознакомились с полным описанием проекта в предложении (см. раздел Описание проекта и дополнительная литература ниже), вот перечень недостающих возможностей.

Полиморфизм по кратности реализован не полностью и является экспериментальным. Возможно, вам удастся его использовать, а возможно, нет. Ожидайте крайне ненадёжного поведения. (Умножение кратностей пока не поддерживается.)
В настоящее время нет поддержки аннотаций кратности для аргументов функций, например \(%p x :: a) -> ...; аннотации доступны только для переменных, связанных через let.
Выражение case может потребить проверяемое значение One раз или Many раз. Однако вывод всё ещё экспериментальный и может слишком поспешно предположить, что проверяемое значение нужно потребить Many раз.
Линейные синонимы образцов не поддерживаются.
Образцы @ и образцы-представления не являются линейными.
Функция проекции для записи с единственным линейным полем должна иметь полиморфизм по кратности; в настоящее время она не ограничена.
Попытка использовать линейные типы в Template Haskell, вероятно, не сработает.

6.4.22.5. Описание проекта и дополнительная литература

Описание проекта этого расширения подробно изложено в предложении о линейных типах
Изначально это расширение было предложено в статье Linear Haskell: практическая линейность в полиморфном языке высшего порядка (POPL 2018)
Существует вики-страница, посвящённая расширению линейных типов

© 2002–2007 The University Court of the University of Glasgow. All rights reserved.
Licensed under the Glasgow Haskell Compiler License.
https://downloads.haskell.org/~ghc/9.14.1/docs/users_guide/exts/linear_types.html