>> придётся и setsockopt() настраивать Так или иначе, придётся его настраивать. С зависимыми типами можно сделать ему такой интерфейс, что настройки и вызовы функций будут консистентными, что гарантируется на этапе компиляции. Например, если нет куска кода, который устанавливает SO_ACCEPTCONN, сокет нельзя будет слушать.
>> а если с БД -- то проверять схему БД на соответствие схеме, которую "умеет" программа, и тоже в рантайме. Эти проверки можно автоматически генерировать из типов, чтобы не писать их самому. Без зависимых типов - попоболь.
>> То есть, и проверки, и тесты -- будут, от них никуда не деться. От них никуда не деться по той простой причине, что любой важный (ЖД, медицина, военпром) софт обязан тестироваться по стандартам. В принципе, зависимые типы не могут отфильтровать очень хитрые логические ошибки, но никакие проверки и тесты в таких случаях всё равно не помогут.
>> Но XSD и подобное -- оно, бывает, должно загружаться в программу из интернетов / с диска, тут типами ничего не ограничить. А вот и нет :) Здесь ключевое слово - type directed computation. Методы для работы с XSD не откомпилируются, пока они не станут кушать все возможные граничные случаи. Методы, работающие с представлением XSD внутри программы, не откомпилируются, пока не научатся употреблять все возможные XSD.
>> надо какую-то версионность и "переходники" лепить Комбинаторный стиль для того и сделан, чтобы как можно реже (т.е. никогда) не менять уже готовую функцию. Проблемы возникают в случае, если ты хочешь, чтобы у тебя версионность относилась к какому-нибудь FFI или работе с файлами собственного формата. Эта часть в зависимо типизированных языках вообще не проработана. Для файлов я бы порекомендовал пользоваться каким-нибудь XML'ем, который, конечно, говно, но позволяет кое-какую версионность проталкивать на уровне стандарта формата.
>> Ну и кодогенерация таким же образом полезна. Одно -- частный случай другого, понимаю тоже. Да не частный случай, это вообще одно и то же. Только зависимые типы работают, а рукописные кодогенераторы нет.
>> нужно дать возможность бухгалтерам совершать проводки с отрицательной суммой, нужно считать торговую наценку на товар не прямым образом, а через две пизды, связанные с округлением до копеек, что нужно считать не сумму по количеству и цене, а цену по сумме и количеству, и все эти ограничения, которые любовно выписывались в виде теорем-утверждений, приходится выкидывать или переписывать. 1. Делаем функции более абстрактными (с параметрами типа), чуя жопой, что integer может замениться на unsigned и т.п. 2. Аналогично, более абстрактными делаем доказательства. 3. В несложных случаях, поручаем доказательства тактикам, забывая о том, что нам вообще нужно что-то передоказывать.
>> и это я вспомнил только 1% от нелогичных вещей, которые мне нужно было реализовывать для того, чтобы мои программы приносили пользу в реаллайфе Сам я пишу на ABAP'е, ну понятно, да?
>> (плюс структурным созданием/разрушением типов данных) Вот эта штука с зависимыми типами ну просто волшебно выглядит.
>> Может просто я не академик, и мои задачи вообще надо на похапэ решать? Или как вообще жить? Именно в поисках ответа на этот вопрос я хочу узнать про зависимые типы, про их практические применения. Имхо, нужно просто сесть и начать с ними писать. Либо вы поймёте, что это вам полезно, либо сможете предложить, как их можно улучшить. По-моему, штука полностью практическая.
> Например, если нет куска кода, который устанавливает 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. Например, можно выделять замыкания в куче, и потом компилятор заставит нас их освободить.
Эта мысль "Комбинаторный стиль для того и сделан, чтобы как можно реже (т.е. никогда) не менять уже готовую функцию" очень порадовала (не сарказм). Это интуитивное ощущение или она была где-то развёрнуто сформулирована?
Так или иначе, придётся его настраивать. С зависимыми типами можно сделать ему такой интерфейс, что настройки и вызовы функций будут консистентными, что гарантируется на этапе компиляции. Например, если нет куска кода, который устанавливает SO_ACCEPTCONN, сокет нельзя будет слушать.
>> а если с БД -- то проверять схему БД на соответствие схеме, которую "умеет" программа, и тоже в рантайме.
Эти проверки можно автоматически генерировать из типов, чтобы не писать их самому. Без зависимых типов - попоболь.
>> То есть, и проверки, и тесты -- будут, от них никуда не деться.
От них никуда не деться по той простой причине, что любой важный (ЖД, медицина, военпром) софт обязан тестироваться по стандартам. В принципе, зависимые типы не могут отфильтровать очень хитрые логические ошибки, но никакие проверки и тесты в таких случаях всё равно не помогут.
>> Но XSD и подобное -- оно, бывает, должно загружаться в программу из интернетов / с диска, тут типами ничего не ограничить.
А вот и нет :) Здесь ключевое слово - type directed computation. Методы для работы с XSD не откомпилируются, пока они не станут кушать все возможные граничные случаи. Методы, работающие с представлением XSD внутри программы, не откомпилируются, пока не научатся употреблять все возможные XSD.
>> надо какую-то версионность и "переходники" лепить
Комбинаторный стиль для того и сделан, чтобы как можно реже (т.е. никогда) не менять уже готовую функцию. Проблемы возникают в случае, если ты хочешь, чтобы у тебя версионность относилась к какому-нибудь FFI или работе с файлами собственного формата. Эта часть в зависимо типизированных языках вообще не проработана. Для файлов я бы порекомендовал пользоваться каким-нибудь XML'ем, который, конечно, говно, но позволяет кое-какую версионность проталкивать на уровне стандарта формата.
>> Ну и кодогенерация таким же образом полезна. Одно -- частный случай другого, понимаю тоже.
Да не частный случай, это вообще одно и то же. Только зависимые типы работают, а рукописные кодогенераторы нет.
>> нужно дать возможность бухгалтерам совершать проводки с отрицательной суммой, нужно считать торговую наценку на товар не прямым образом, а через две пизды, связанные с округлением до копеек, что нужно считать не сумму по количеству и цене, а цену по сумме и количеству, и все эти ограничения, которые любовно выписывались в виде теорем-утверждений, приходится выкидывать или переписывать.
1. Делаем функции более абстрактными (с параметрами типа), чуя жопой, что integer может замениться на unsigned и т.п.
2. Аналогично, более абстрактными делаем доказательства.
3. В несложных случаях, поручаем доказательства тактикам, забывая о том, что нам вообще нужно что-то передоказывать.
>> и это я вспомнил только 1% от нелогичных вещей, которые мне нужно было реализовывать для того, чтобы мои программы приносили пользу в реаллайфе
Сам я пишу на ABAP'е, ну понятно, да?
>> (плюс структурным созданием/разрушением типов данных)
Вот эта штука с зависимыми типами ну просто волшебно выглядит.
>> Может просто я не академик, и мои задачи вообще надо на похапэ решать? Или как вообще жить? Именно в поисках ответа на этот вопрос я хочу узнать про зависимые типы, про их практические применения.
Имхо, нужно просто сесть и начать с ними писать. Либо вы поймёте, что это вам полезно, либо сможете предложить, как их можно улучшить. По-моему, штука полностью практическая.
Reply
ну так это можно закодировать и простым соответствием функций и утверждений:
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
Reply
Есть, конечно, Numeric Prelude и Awesome Prelude, но это не переписывание имеющегося кода, это вообще другие библиотеки.
Reply
Leave a comment