-
LinearTypes -
- Подразумевает:
- С:
-
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.21.1. Выражения
При определении функции как лямбда-выражения \x -> u или с уравнениями f x = u, кратность переменной x будет вычислена из контекста. Для уравнений контекст обычно будет сигнатурой типа. Например, вот линейная функция
f :: (a -> b) %1 -> a -> b f g x = g x
В этом примере g должна использоваться линейно, в то время как x неограниченна.
6.4.21.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.21.1.2. Строгие образцы
GHC считает, что ленивые образцы, не являющиеся переменными, потребляют объект сопоставления с кратностью Many. На практике образец является строгим (следовательно, может быть линейным), если (в противном случае образец является ленивым):
- Образец является альтернативой случая и не аннотирован
~ - Образец является связыванием 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.21.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 T3 a m where
MkT3 :: a %m -> T3 a m
Хотя линейные поля обобщаются (MkT1 :: forall {m} a. a %m -> T1 a в предыдущем примере), поля с полиморфизмом по кратности нет; напрямую использовать MkT3 как функцию a -> T3 a One нельзя.
Если LinearTypes отключен, все поля считаются линейными полями, включая поля GADT, определённые с помощью стрелки ->.
В объявлении newtype поле должно быть линейным. Попытка написать неограниченный конструктор newtype с синтаксисом GADT приводит к ошибке.
6.4.21.3. Вывод типов полиморфных по кратности
Если LinearTypes отключен, переменные кратности в типах по умолчанию устанавливаются в Many при выводе, так же как описано в Вывод типов с полиморфизмом представлений. Иными словами, без LinearTypes полиморфные по кратности функции a %m -> b выводятся как обычные функции Haskell2010 a -> b. Это позволяет обобщить существующие библиотеки на линейные типы в обратной совместимой форме; обобщённые типы видны только если пользователь включил LinearTypes. (Обратите внимание, что библиотека может объявить линейную функцию в контравариантной позиции, т.е. принять линейную функцию в качестве аргумента. В этом случае линейность нельзя скрыть; она является неотъемлемой частью опубликованного интерфейса.)
