> Например, если нет куска кода, который устанавливает SO_ACCEPTCONN, сокет нельзя будет слушать.
ну так это можно закодировать и простым соответствием функций и утверждений:
module Sock : sig type socket = Unix.file_descr; type listening_socket; value listen : socket -> backlog:int -> listening_socket; value accept : listening_socket -> (socket * sock_addr); end; если не вызвали listen -- не на чём будет вызвать accept. То есть, конкретно в этом случае зависимые типы не очень полезны. Хотя идею понял.
>> >> а если с БД -- то проверять схему БД на соответствие схеме, которую "умеет" программа, и тоже в рантайме. >> Эти проверки можно автоматически генерировать из типов, чтобы не писать их самому. Без зависимых типов - попоболь.
согласен, что простой подход не очень подходит тут. Но я подобную проблему решил "динамикой": для каждого нужного типа создаётся рантайм-описание значений этого типа, и вот, из них вполне можно генерить как проверку схемы бд, так и типизированный интерфейс наподобие "вот имя таблицы бд, вот описание типов, сделай мне fold по всем строкам таблицы". Пока хватает такого.
>> А вот и нет :) Здесь ключевое слово - type directed computation. Методы для работы с XSD не откомпилируются, пока они не станут кушать все возможные граничные случаи. Методы, работающие с представлением XSD внутри программы, не откомпилируются, пока не научатся употреблять все возможные XSD.
Тогда я недопонял. Что в случае с XSD известно на момент компиляции, и что может быть "добавлено" потом, в рантайме?
>> Сам я пишу на ABAP'е, ну понятно, да?
Приношу свои искренние соболезнования. Не думал, что эта тема (с бухгалтерией всякой) будет проходить так близко от недавнего и длящегося горя. Не поднимал бы её.
>> >> (плюс структурным созданием/разрушением типов данных) >> Вот эта штука с зависимыми типами ну просто волшебно выглядит.
А есть какие-нибудь годные примеры, не слишком сложные, но кое-как показывающие это?
Насчет примера с сокетом меня в ATS порадовало применение линейных типов для утверждений. Они не только заботятся о том, чтобы не читать из не того сокета, они также не дадут забыть закрыть сокет, например. Открыли сокет/файл/вотева - получили доказательство этого факта, и за счет его линейности мы во-первых не можем его использовать повторно после того, как "потратили" (закрыв файл/сокет), а во-вторых мы обязаны его "потратить", иначе прога не компилируется. Но это вроде не относится напрямую именно к зависимым типам, это несколько другая фича.
Если коротко, главная и основная черта линейных типов - их значения нельзя дублировать. Значение можно создать, можно разрушить (паттерн-матчингом), можно передать в функцию или вернуть, но если х : L, где L - линейный тип, то нельзя построить тупл (х,х) или выражение f x + g x или другое выражение, где х встречается более одного раза. Очень похоже на уникальные типы в Clean, но с небольшими отличиями (в Clean при определенных условиях дублирование допустимо - когда мы только читаем, но не пишем). Если мы передали значение линейного типа в функцию, то все, у нас его больше нет, мы его "потратили". Функция может вернуть его или новое значение обратно. Так функции, работающие со значениями линейных/уникальных типов, естественным образом выстраиваются в цепочку с четким порядком - сначала с этим значением работает такая-то функция, потом, когда она его вернет, такая-то. Это позволило в Clean сделать ввод-вывод безо всяких монад.
В ATS есть сорт линейных типов-утверждений, называется view. Такие типы выглядят как простые алгебраические типы, но в силу их линейности созданное значение можно туда-сюда передавать, но не размножать. А еще, в отличие от типов данных сортов type и t@ype, при компиляции они полностью исчезают, в рантайме этих значений нигде нет. И еще есть механизм для связывания view и данных: на значение некоторого типа данных можно навесить какой-нибудь вид (линейное утверждение). Например, "этот файловый дескриптор открыт на запись", или "по этому указателю буфер из n непроинициализированных интов". Функция записи в файл требует такую вот пару - файловый дескриптор с навешенным на него видом, подтверждающим, что файл открыт на запись. Функция закрытия файла берет похожую пару, но обратно вид не возвращает, поэтому больше мы файловый дескриптор использовать не можем. А еще ATS, отслеживая операции с линейными значениями, требует, чтобы они были разрушены, "потрачены". Это можно сделать либо передав в функцию, которая не вернет его обратно (вроде закрытия файла или освобождения памяти), либо паттерн-матчингом, но если этот тип для нас абстрактный и его настоящую структуру знает только чужой модуль, то паттерн-матчинг нам недоступен, так что ничего не поделаешь, придется файл закрыть. Этот же механизм используется для работы без GC. Например, можно выделять замыкания в куче, и потом компилятор заставит нас их освободить.
ну так это можно закодировать и простым соответствием функций и утверждений:
module Sock
:
sig
type socket = Unix.file_descr;
type listening_socket;
value listen : socket -> backlog:int -> listening_socket;
value accept : listening_socket -> (socket * sock_addr);
end;
если не вызвали listen -- не на чём будет вызвать accept.
То есть, конкретно в этом случае зависимые типы не очень полезны. Хотя идею понял.
>> >> а если с БД -- то проверять схему БД на соответствие схеме, которую "умеет" программа, и тоже в рантайме.
>> Эти проверки можно автоматически генерировать из типов, чтобы не писать их самому. Без зависимых типов - попоболь.
согласен, что простой подход не очень подходит тут. Но я подобную проблему решил "динамикой": для каждого нужного типа создаётся рантайм-описание значений этого типа, и вот, из них вполне можно генерить как проверку схемы бд, так и типизированный интерфейс наподобие "вот имя таблицы бд, вот описание типов, сделай мне fold по всем строкам таблицы". Пока хватает такого.
>> А вот и нет :) Здесь ключевое слово - type directed computation. Методы для работы с XSD не откомпилируются, пока они не станут кушать все возможные граничные случаи. Методы, работающие с представлением XSD внутри программы, не откомпилируются, пока не научатся употреблять все возможные XSD.
Тогда я недопонял. Что в случае с XSD известно на момент компиляции, и что может быть "добавлено" потом, в рантайме?
>> Сам я пишу на ABAP'е, ну понятно, да?
Приношу свои искренние соболезнования. Не думал, что эта тема (с бухгалтерией всякой) будет проходить так близко от недавнего и длящегося горя. Не поднимал бы её.
>> >> (плюс структурным созданием/разрушением типов данных)
>> Вот эта штука с зависимыми типами ну просто волшебно выглядит.
А есть какие-нибудь годные примеры, не слишком сложные, но кое-как показывающие это?
Reply
Reply
Reply
Если коротко, главная и основная черта линейных типов - их значения нельзя дублировать. Значение можно создать, можно разрушить (паттерн-матчингом), можно передать в функцию или вернуть, но если х : L, где L - линейный тип, то нельзя построить тупл (х,х) или выражение f x + g x или другое выражение, где х встречается более одного раза. Очень похоже на уникальные типы в Clean, но с небольшими отличиями (в Clean при определенных условиях дублирование допустимо - когда мы только читаем, но не пишем). Если мы передали значение линейного типа в функцию, то все, у нас его больше нет, мы его "потратили". Функция может вернуть его или новое значение обратно. Так функции, работающие со значениями линейных/уникальных типов, естественным образом выстраиваются в цепочку с четким порядком - сначала с этим значением работает такая-то функция, потом, когда она его вернет, такая-то. Это позволило в Clean сделать ввод-вывод безо всяких монад.
В ATS есть сорт линейных типов-утверждений, называется view. Такие типы выглядят как простые алгебраические типы, но в силу их линейности созданное значение можно туда-сюда передавать, но не размножать. А еще, в отличие от типов данных сортов type и t@ype, при компиляции они полностью исчезают, в рантайме этих значений нигде нет. И еще есть механизм для связывания view и данных: на значение некоторого типа данных можно навесить какой-нибудь вид (линейное утверждение). Например, "этот файловый дескриптор открыт на запись", или "по этому указателю буфер из n непроинициализированных интов". Функция записи в файл требует такую вот пару - файловый дескриптор с навешенным на него видом, подтверждающим, что файл открыт на запись. Функция закрытия файла берет похожую пару, но обратно вид не возвращает, поэтому больше мы файловый дескриптор использовать не можем. А еще ATS, отслеживая операции с линейными значениями, требует, чтобы они были разрушены, "потрачены". Это можно сделать либо передав в функцию, которая не вернет его обратно (вроде закрытия файла или освобождения памяти), либо паттерн-матчингом, но если этот тип для нас абстрактный и его настоящую структуру знает только чужой модуль, то паттерн-матчинг нам недоступен, так что ничего не поделаешь, придется файл закрыть. Этот же механизм используется для работы без GC. Например, можно выделять замыкания в куче, и потом компилятор заставит нас их освободить.
Reply
Ещё одна область, где в каких-то частях программы очень может быть полезно доказательство, это всякое параллельное.
Reply
Leave a comment