Линейные типы:

ru_lambda — 25.09.2011 Один из сообщников у себя в блоге задает вопрос "уже кто-нибудь усвоил линейную логику в программировании?". Разумеется давно (лет 20 назад) освоили: позволю пару ссылок на Wiki - "Linear types" и "Clean" (Clean если кто не знает - язык очень близкий к Haskell и отличающийся от него пожалуй в основном как раз подходом к трактовке mutable states - именно для этого там и юзаются линейные типы) и на список публикаций Software Technology group of the MBSD section of the CS department of the University of Nijmegen (искать по ключевым словам "linear type" и "unique type").

Идея проста и довольно продуктивна (хотя пока толком почему-то не востребована):

Любой тип может иметь модификатор линейности (в clean она называется "уникальностью") - скажем Int и *Int. "Уникальность" означает, что на данное значение в данный момент времени существует единственная ссылка (а система типов это гарантирует) - если примитивно - то переменную уникального типа можно передать параметром только один раз функцию, а система типов этот контроль обеспечивает (в первом приближении - проверяя что все ее испльзования взаимоисключающие с точки зрения потока данных).

Применений у них два: первое обслуживает ввод-вывод - в Clean не используются монадыю Вместо этого есть тип World(символизирующий окружающий мир), функция Start (аналог main) имеет тип

Start:: *World -> *World,

и есть функции, "отщепляющие" из мира разные другие сущности - файлы, "мир гуевых событий" etc. Выглядит это примерно так:

module test
import StdEnv, StdFile

Start :: *World -> *World
Start world = 
  let (ok,file,world1) = fopen "test.file" FWriteText world in
  let file1 = Process file in
  let (ok,world2) = fclose file1 world1 in
  world2

Process :: *File -> *File
Process file = 
  let file1 = fwrites "Hello,\n" file  in
  let file2 = fwrites "World\n"  file1 in
  file2

функция fopen "отщепляет" *File от *World,возвращая статус, и "новый" *World, fwrites пишет в *File строчку, возвращая "новый" *File. Ну а fclose "вливает" файл обратно "в большой мир"

При попытке использовать "старый" file еще раз будет диагностика времени компиляции:

Uniqueness error: "xxx" demanded attribute cannot be offered by shared object

Обращу внимание на то, что в операция fclose тут необходима вовсе не только в привычном нам смысле сброса буферов etc - если не влить *File обратно в *World - тот как и следует ожидать останется неизмененным - файл даже не создастся: если отвлечься от абстрактных причин - язык ленивый и если значение file1 не будет затребовано - никаких действий ведущих к его вычислению не будет и проделано.

Разумеется такую жуть пишут редко - имеется куча всякого синтаксисического сахара - например - операция <<<:

class (<<<) infixl a :: !*File !a -> *File
instance <<< Char
instance <<< Int
...

и вместо

let file1 = Process file in
let (ok,world2) = fclose file1 world1 in

Можно просто написать

let (ok,world2) = fclose (file <<< "Hello," <<< "world\n") world1 in

Ну и другие украшательства есть.

Помимо "ввода-вывода" у линейных типов в Clean есть еще одно важное применение: эффективная работа с изменямыми агрегатными данными:

module test2
import StdEnv, StdArray

Start :: *World -> {Int}
Start world =  update (createArray 10 1) 5 10 

Напечатает

{1,1,1,1,1,10,1,1,1,1}

В отличие от Haskell операция update тут не вызовет копирования массива:

class Array a e where
  update :: *(a e) Int e → *(a e)  
  createArray :: !Int e -> *(a e)

Ну и последнее - полиморфизм по свойству линейности тип операции конкатенации списков выглядит так:

(++) infixr 5 :: [u:a] w:[u:a] -> v:[u:a], [w<=v]

Что означает, что ++ полиморфна по уникальности типа эемента списков (при этом этот атрибут должен быть одинаков у всех*). Запись же [w<=v] означает, что если результат конкатенации должен быть уникален, то второй аргумент ++ также олжен быть уникальным списком.

PS: Изложение, разумеется, упрощенное - за деталями - в статьи или в четвертую главу описания Clean.

Upd: поскольку с ленивостью возникли непонятки, еще пример:

Process :: Bool *File -> *File
Process b file = 
  let file1 = fwrites "Hello,\n" file  in
  let file2 = fwrites "World\n"  file1 in
  let file3 = fwrites "Galaxy\n" file1 in
  if b file2 file3

В зависимости от первого аргумента в file будет записано либо "Hello, World" либо "Hello, Galaxy"

---

*) поскольку значение уникального типа может быть использовано как значение обычного типа - на практике это означает, что если хоть в одном из типов списков элемент не уникален - не уникальны они все

Оставить комментарий

Популярные посты: