gds

dependent types

Mar 05, 2012 15:17

(как бы разворачивая каменты из предыдущего поста ( Read more... )

Leave a comment

thedeemon March 6 2012, 18:03:04 UTC
Поподробнее отдельным постом отпишусь чуть позже.

Если коротко, главная и основная черта линейных типов - их значения нельзя дублировать. Значение можно создать, можно разрушить (паттерн-матчингом), можно передать в функцию или вернуть, но если х : L, где L - линейный тип, то нельзя построить тупл (х,х) или выражение f x + g x или другое выражение, где х встречается более одного раза. Очень похоже на уникальные типы в Clean, но с небольшими отличиями (в Clean при определенных условиях дублирование допустимо - когда мы только читаем, но не пишем). Если мы передали значение линейного типа в функцию, то все, у нас его больше нет, мы его "потратили". Функция может вернуть его или новое значение обратно. Так функции, работающие со значениями линейных/уникальных типов, естественным образом выстраиваются в цепочку с четким порядком - сначала с этим значением работает такая-то функция, потом, когда она его вернет, такая-то. Это позволило в Clean сделать ввод-вывод безо всяких монад.

В ATS есть сорт линейных типов-утверждений, называется view. Такие типы выглядят как простые алгебраические типы, но в силу их линейности созданное значение можно туда-сюда передавать, но не размножать. А еще, в отличие от типов данных сортов type и t@ype, при компиляции они полностью исчезают, в рантайме этих значений нигде нет. И еще есть механизм для связывания view и данных: на значение некоторого типа данных можно навесить какой-нибудь вид (линейное утверждение). Например, "этот файловый дескриптор открыт на запись", или "по этому указателю буфер из n непроинициализированных интов". Функция записи в файл требует такую вот пару - файловый дескриптор с навешенным на него видом, подтверждающим, что файл открыт на запись. Функция закрытия файла берет похожую пару, но обратно вид не возвращает, поэтому больше мы файловый дескриптор использовать не можем. А еще ATS, отслеживая операции с линейными значениями, требует, чтобы они были разрушены, "потрачены". Это можно сделать либо передав в функцию, которая не вернет его обратно (вроде закрытия файла или освобождения памяти), либо паттерн-матчингом, но если этот тип для нас абстрактный и его настоящую структуру знает только чужой модуль, то паттерн-матчинг нам недоступен, так что ничего не поделаешь, придется файл закрыть. Этот же механизм используется для работы без GC. Например, можно выделять замыкания в куче, и потом компилятор заставит нас их освободить.

Reply

nivanych March 8 2012, 06:47:24 UTC
Да вот, вспомнилось.
Ещё одна область, где в каких-то частях программы очень может быть полезно доказательство, это всякое параллельное.

Reply


Leave a comment

Up
[]