Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет kouzdra ([info]kouzdra)
@ 2011-09-25 11:27:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Линейные типы:
X-Post from: http://ru-lambda.livejournal.com/131849.html

Один из сообщников у себя в блоге задает вопрос "уже кто-нибудь усвоил линейную логику в программировании?". Разумеется давно (лет 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.

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


(Добавить комментарий)

offtop - буду благодарен, если ответите
[info]ende_neu
2011-09-27 21:34 (ссылка)
А вы не в курсе, как обстоят дела с образованием в Computer Science в Германии? В частности, не слышали ли вы что-нибудь хорошее/плохое о Боннском университете? И какие там еще хорошие места по этой науке имеются (ну, кроме Technische Universität München, который и так ясно, что круче всех, по рейтингам, по крайней мере)?

И еще - какова в этой области роль архив.орг? Такая же, как и в математике (то есть очень многое из существенного выкладывается туда) или существенно скромнее?

(Ответить) (Ветвь дискуссии)

Re: offtop - буду благодарен, если ответите
[info]kouzdra
2011-09-29 21:57 (ссылка)
Совершенно не в курсе - из чего наверное некоторые ненадежные выводы можно сделать (Clean - это голландцы)

(Ответить) (Уровень выше) (Ветвь дискуссии)

Re: offtop - буду благодарен, если ответите
[info]ende_neu
2011-09-30 21:18 (ссылка)
Ясно, да, выводы неприятные :)
Спасибо.

(Ответить) (Уровень выше)