| |||
|
|
Линейные типы: X-Post from: http://ru-lambda.livejournal.com/13 Один из сообщников у себя в блоге задает вопрос "уже кто-нибудь усвоил линейную логику в программировании?". Разумеется давно (лет 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. *) поскольку значение уникального типа может быть использовано как значение обычного типа - на практике это означает, что если хоть в одном из типов списков элемент не уникален - не уникальны они все |
||||||||||||||