есть некоторые комментарии, "я хочу об этом поговорить".
1. в случае единиц измерения -- лично мне было достаточно либо подхода "складываем-вычитаем однотипное, есть специальные функции для умножения массы на скорость", либо подхода "носим единицы измерения в рантайме", либо, для непересекающихся единиц измерения, подход "по одному типу на каждую единицу измерения". первое -- для надёжных вещей, второе -- для остального, что в рантайме всяко высветится (ну и тесты, как же без них), третье -- просто абстрактные типы, вполне удобно, если не ставить больших целей. Так вот, самый слабый подход -- держать всё в рантайме. Но я не представляю, как можно написать что-то большое (не просто отдельный мелкий модуль) так, чтобы вообще не тестировать. На худой конец, если программа работает с сетью, придётся и setsockopt() настраивать, а если с БД -- то проверять схему БД на соответствие схеме, которую "умеет" программа, и тоже в рантайме. То есть, и проверки, и тесты -- будут, от них никуда не деться. Их количество -- да, другой вопрос. Но так, чтобы можно было всё изначально вывести из спецификации -- лично я сомневаюсь. Для игрушечных случаев -- конечно получится, тут не спорю, а для реальных? Кроме того, о подобных вещах я написал и ниже.
2. про DSL -- принято. Это действительно хорошо. Но XSD и подобное -- оно, бывает, должно загружаться в программу из интернетов / с диска, тут типами ничего не ограничить (либо ограничить можно, но, всё равно, разборки только в рантайме). Бывает так, что XSD или другое определение данных внезапно меняется. Типы тут становятся не очень хороши -- либо надо какую-то версионность и "переходники" лепить, либо вообще логику переписывать, ту, которая работает с значениями этих типов. Для случая "задрочить одно определение данных и написать под него безглючный код" -- да, зависимые типы рулят, я согласен. Ну и кодогенерация таким же образом полезна. Одно -- частный случай другого, понимаю тоже.
3. логику -- уважаю, coq -- использовал (но для забавы, скорее). Про ограничения на программу -- согласен, что они нужны. Но даже в сраных языках программирования без зависимых типов оказывается так, что, налепив типы и начав делать дела, тех.задание меняется быстрее реализации, какие-то детали реализации тоже меняются (например, использовали одну библиотеку для доступа к бд, а теперь другая), внезапно оказалось, что нужно дать возможность бухгалтерам совершать проводки с отрицательной суммой, нужно считать торговую наценку на товар не прямым образом, а через две пизды, связанные с округлением до копеек, что нужно считать не сумму по количеству и цене, а цену по сумме и количеству, и все эти ограничения, которые любовно выписывались в виде теорем-утверждений, приходится выкидывать или переписывать. Это демотивирует. (и это я вспомнил только 1% от нелогичных вещей, которые мне нужно было реализовывать для того, чтобы мои программы приносили пользу в реаллайфе. я пытаюсь забыть всё это, у меня пока получается.)
Вот я и пытаюсь понять, где же для моих задач будут полезны зависимые типы. Где полезна строгая типизация (кстати, я камлоёб) -- я разобрался, да и то, то всякие аппликативные функторы для доступа к реляционкам использую с проверками в рантайме, то вообще динамику налепил поверх окамла, и она реально помогает, кучу задач решил ею (плюс структурным созданием/разрушением типов данных), аж чуть ли не дрочу на неё. Может просто я не академик, и мои задачи вообще надо на похапэ решать? Или как вообще жить? Именно в поисках ответа на этот вопрос я хочу узнать про зависимые типы, про их практические применения.
Тесты - это утверждения о коде, проверяемые на частных случаях и без гарантии полноты. И проверяемые после компиляции, в рантайме. Завтипы позволяют большую часть утверждений перенести в компайл-тайм, причем вместо частных случаев там будут общие. Получается, что как бы цель одна (проверка утверждений), но реализация и ее качество/полнота разные.
Соответственно, если часто меняются требования, то либо нужно постоянно тратить время на обновление тестов и их проверку, либо на обновление теорем (там проверкой занимается компилятор). Первый подход проще и позволяет быстрее выдать какой-то код, который иногда работает. Второй подход сложнее и дает какой-то код только когда он будет всегда работать.
Завтипы требуют писать хороший код, иначе он не компилируется. Это обычно сложнее и дольше, чем просто писать код. Плюс, порой вещи, которые нам кажутся очевидными, компилятору совсем не очевидны, приходится ему подробно доказывать, это тоже требует лишнего времени (но иногда может быть оправдано, ибо слово "кажутся" там неспроста). Поэтому в ряде областей выигрыша по времени и трудозатратам не будет.
Иначе говоря, надо развивать автоматическое доказательство, ну хоть бы и по мелочам. В агде-2.2.6 оно было малопригодно (а может быть, я недостаточно попарился и не научился готовить). Агду-2.3 надо смотреть, но я сомневаюсь, что в этом направлении что-то существенно изменилось. Если пытаться использовать агду, как "обычный" язык с выводом типов, как хацкель, то отличие одно и существенное (и даже вовсе не в классах типов) - совершенно другой подход к работе с выводом типов (неявные параметры), и привыкать к нему непросто. Вроде, в новых агдах понаделали в этом направлении поболее, навроде таки попыток вывода, когда это возможно. Но всё равно, по-другому всё.
Дилетантское видение? Человека, который смог связать что-то сложнее хелловорлда на ATS'е? Ребе, да вам нужно памятник поставить за скромность.
>> которые нам кажутся очевидными Ага, недавно читал статью о представлении чисел в зависимо типизированном языке. Там говорилось, что через несколько месяцев исследований автор узнал о числах намного больше, чем ожидал :)
Это означает только бОльшую простоту программирования в агде ;-) Я вот только смотрел исходники, но сам не пытался писать. Тут же уже есть хоть какой-то опыт с пониманием. Довольно согласующийся с тем, что я прикидывал.
про изменение требований -- получается, в тестах будут вместо теста A=success -- два теста A=failure (изменённая функциональность работает по-другому) и B=success. В случае быстрого написания, очевидно, проще добавить тест и поддерживать их кучу, причём нахаляву и без особых проблем. В случае доказательства кода для эквивалентного "покрытия доказательствами" нужно будет доказывать как A=False, так и B=True, а то и переписывать код и доказательства. То есть, для каждого куска задачи нужно решать, использовать там тесты и вероятность фейла в рантайме, или доказывать по-честному.
> обновление теорем (там проверкой занимается компилятор)
сначала ещё теорему надо написать и доказать. Тоже время.
> дает какой-то код только когда он будет всегда работать.
это если исходные аксиомы и теоремы сформулированы правильно. Получается, тут вместо простого написания и обдумывания кода пишется и обдумывается спецификация, и только потом пишется код. Источник ошибок в виде человеческого фактора остаётся, только передвигается на момент написания спецификации. То есть, хрен редьки не толще.
всё остальное понял, благодарен за помощь в "устаканивании" этого дела в пределах моей головы.
Верно, написание теорем требует времени и сил, много. Зато покрытие дает более полное, чем тесты. Такой вот выбор между уверенностью в корректности и быстротой написания.
Что касается человеческого фактора, то у меня пока такое ощущение сложилось, что он в случае снабжения кода теоремами/утверждениями сильно меньше, т.к. код и утверждения обязяны быть согласованы, чтобы это скомпилировалось, а допустить одну и ту же ошибку, да такую, которая не будет противоречить другим теориям, очень сложно. Если в простом коде или тесте легко написать глупость, то тут компилятор не даст ее так просто даже сформулировать. Конечно, еще остается возможность ошибки высокого уровня: когда предметная область понята неправильно и сформулированы и доказаны не те теоремы, код делает не то, хоть и делает это правильно. Тут да, исправление потребует бОльших усилий.
> Такой вот выбор между уверенностью в корректности и быстротой написания.
Кроме того, с возможностью баллансировать сколько угодно. Можно и просто список использовать с целыми числами, можно с типом-параметром, а можно ещё и с длиной, а можно и куда-то передать значение типа доказательств, что длина какая-нибудь (не) такая.
>> придётся и 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 порадовало применение линейных типов для утверждений. Они не только заботятся о том, чтобы не читать из не того сокета, они также не дадут забыть закрыть сокет, например. Открыли сокет/файл/вотева - получили доказательство этого факта, и за счет его линейности мы во-первых не можем его использовать повторно после того, как "потратили" (закрыв файл/сокет), а во-вторых мы обязаны его "потратить", иначе прога не компилируется. Но это вроде не относится напрямую именно к зависимым типам, это несколько другая фича.
есть некоторые комментарии, "я хочу об этом поговорить".
1. в случае единиц измерения -- лично мне было достаточно либо подхода "складываем-вычитаем однотипное, есть специальные функции для умножения массы на скорость", либо подхода "носим единицы измерения в рантайме", либо, для непересекающихся единиц измерения, подход "по одному типу на каждую единицу измерения". первое -- для надёжных вещей, второе -- для остального, что в рантайме всяко высветится (ну и тесты, как же без них), третье -- просто абстрактные типы, вполне удобно, если не ставить больших целей.
Так вот, самый слабый подход -- держать всё в рантайме. Но я не представляю, как можно написать что-то большое (не просто отдельный мелкий модуль) так, чтобы вообще не тестировать. На худой конец, если программа работает с сетью, придётся и setsockopt() настраивать, а если с БД -- то проверять схему БД на соответствие схеме, которую "умеет" программа, и тоже в рантайме. То есть, и проверки, и тесты -- будут, от них никуда не деться. Их количество -- да, другой вопрос. Но так, чтобы можно было всё изначально вывести из спецификации -- лично я сомневаюсь. Для игрушечных случаев -- конечно получится, тут не спорю, а для реальных? Кроме того, о подобных вещах я написал и ниже.
2. про DSL -- принято. Это действительно хорошо.
Но XSD и подобное -- оно, бывает, должно загружаться в программу из интернетов / с диска, тут типами ничего не ограничить (либо ограничить можно, но, всё равно, разборки только в рантайме). Бывает так, что XSD или другое определение данных внезапно меняется. Типы тут становятся не очень хороши -- либо надо какую-то версионность и "переходники" лепить, либо вообще логику переписывать, ту, которая работает с значениями этих типов. Для случая "задрочить одно определение данных и написать под него безглючный код" -- да, зависимые типы рулят, я согласен. Ну и кодогенерация таким же образом полезна. Одно -- частный случай другого, понимаю тоже.
3. логику -- уважаю, coq -- использовал (но для забавы, скорее). Про ограничения на программу -- согласен, что они нужны. Но даже в сраных языках программирования без зависимых типов оказывается так, что, налепив типы и начав делать дела, тех.задание меняется быстрее реализации, какие-то детали реализации тоже меняются (например, использовали одну библиотеку для доступа к бд, а теперь другая), внезапно оказалось, что нужно дать возможность бухгалтерам совершать проводки с отрицательной суммой, нужно считать торговую наценку на товар не прямым образом, а через две пизды, связанные с округлением до копеек, что нужно считать не сумму по количеству и цене, а цену по сумме и количеству, и все эти ограничения, которые любовно выписывались в виде теорем-утверждений, приходится выкидывать или переписывать. Это демотивирует. (и это я вспомнил только 1% от нелогичных вещей, которые мне нужно было реализовывать для того, чтобы мои программы приносили пользу в реаллайфе. я пытаюсь забыть всё это, у меня пока получается.)
Вот я и пытаюсь понять, где же для моих задач будут полезны зависимые типы.
Где полезна строгая типизация (кстати, я камлоёб) -- я разобрался, да и то, то всякие аппликативные функторы для доступа к реляционкам использую с проверками в рантайме, то вообще динамику налепил поверх окамла, и она реально помогает, кучу задач решил ею (плюс структурным созданием/разрушением типов данных), аж чуть ли не дрочу на неё.
Может просто я не академик, и мои задачи вообще надо на похапэ решать? Или как вообще жить? Именно в поисках ответа на этот вопрос я хочу узнать про зависимые типы, про их практические применения.
Reply
Тесты - это утверждения о коде, проверяемые на частных случаях и без гарантии полноты. И проверяемые после компиляции, в рантайме.
Завтипы позволяют большую часть утверждений перенести в компайл-тайм, причем вместо частных случаев там будут общие. Получается, что как бы цель одна (проверка утверждений), но реализация и ее качество/полнота разные.
Соответственно, если часто меняются требования, то либо нужно постоянно тратить время на обновление тестов и их проверку, либо на обновление теорем (там проверкой занимается компилятор). Первый подход проще и позволяет быстрее выдать какой-то код, который иногда работает. Второй подход сложнее и дает какой-то код только когда он будет всегда работать.
Завтипы требуют писать хороший код, иначе он не компилируется. Это обычно сложнее и дольше, чем просто писать код. Плюс, порой вещи, которые нам кажутся очевидными, компилятору совсем не очевидны, приходится ему подробно доказывать, это тоже требует лишнего времени (но иногда может быть оправдано, ибо слово "кажутся" там неспроста). Поэтому в ряде областей выигрыша по времени и трудозатратам не будет.
Reply
В агде-2.2.6 оно было малопригодно (а может быть, я недостаточно попарился и не научился готовить).
Агду-2.3 надо смотреть, но я сомневаюсь, что в этом направлении что-то существенно изменилось.
Если пытаться использовать агду, как "обычный" язык с выводом типов, как хацкель, то отличие одно и существенное (и даже вовсе не в классах типов) - совершенно другой подход к работе с выводом типов (неявные параметры), и привыкать к нему непросто. Вроде, в новых агдах понаделали в этом направлении поболее, навроде таки попыток вывода, когда это возможно. Но всё равно, по-другому всё.
Reply
>> которые нам кажутся очевидными
Ага, недавно читал статью о представлении чисел в зависимо типизированном языке. Там говорилось, что через несколько месяцев исследований автор узнал о числах намного больше, чем ожидал :)
Reply
Reply
Reply
Reply
Reply
Я вот только смотрел исходники, но сам не пытался писать.
Тут же уже есть хоть какой-то опыт с пониманием.
Довольно согласующийся с тем, что я прикидывал.
Reply
про изменение требований -- получается, в тестах будут вместо теста A=success -- два теста A=failure (изменённая функциональность работает по-другому) и B=success. В случае быстрого написания, очевидно, проще добавить тест и поддерживать их кучу, причём нахаляву и без особых проблем. В случае доказательства кода для эквивалентного "покрытия доказательствами" нужно будет доказывать как A=False, так и B=True, а то и переписывать код и доказательства. То есть, для каждого куска задачи нужно решать, использовать там тесты и вероятность фейла в рантайме, или доказывать по-честному.
> обновление теорем (там проверкой занимается компилятор)
сначала ещё теорему надо написать и доказать. Тоже время.
> дает какой-то код только когда он будет всегда работать.
это если исходные аксиомы и теоремы сформулированы правильно. Получается, тут вместо простого написания и обдумывания кода пишется и обдумывается спецификация, и только потом пишется код. Источник ошибок в виде человеческого фактора остаётся, только передвигается на момент написания спецификации. То есть, хрен редьки не толще.
всё остальное понял, благодарен за помощь в "устаканивании" этого дела в пределах моей головы.
Reply
Что касается человеческого фактора, то у меня пока такое ощущение сложилось, что он в случае снабжения кода теоремами/утверждениями сильно меньше, т.к. код и утверждения обязяны быть согласованы, чтобы это скомпилировалось, а допустить одну и ту же ошибку, да такую, которая не будет противоречить другим теориям, очень сложно. Если в простом коде или тесте легко написать глупость, то тут компилятор не даст ее так просто даже сформулировать. Конечно, еще остается возможность ошибки высокого уровня: когда предметная область понята неправильно и сформулированы и доказаны не те теоремы, код делает не то, хоть и делает это правильно. Тут да, исправление потребует бОльших усилий.
Reply
Кроме того, с возможностью баллансировать сколько угодно.
Можно и просто список использовать с целыми числами, можно с типом-параметром, а можно ещё и с длиной, а можно и куда-то передать значение типа доказательств, что длина какая-нибудь (не) такая.
Reply
Так или иначе, придётся его настраивать. С зависимыми типами можно сделать ему такой интерфейс, что настройки и вызовы функций будут консистентными, что гарантируется на этапе компиляции. Например, если нет куска кода, который устанавливает 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
Leave a comment