светлое будущее
Mike Potanin potan
Previous Entry Share Next Entry
Где нужны "зависимые типы"?
Все хотят применять "depended types" в разработке больших сложный систем, но мало кто в этом добился хоть каких-нибудь заметных успехов.
Оно и понятно - "зависимые типы" очень усложняют жизнь, а разработкой таких систем занимаются опытные программисты, располагающие развитыми средствами отладки и тестирования. То есть привносимый геморрой не оправдывает потенциальные не слишком радикальные преимущества.
А вот во всяких DSL для конфигурирования, воркфлоу, всяких политик, "умных контрактов" в блокчейнах, скриптов для "интернета вещей", да и просто скриптов для автоматизации рутинной работы чего-то типа "зависимых типов" для обеспечения надежности остро не хватает.
Во первых все эти программы относительно простые, и даже усложнение их разработки в 3-4 раза не так уж и страшно, да и время компиляции от дополнительных проверок сильно не вырастет.
Во вторых средства разработки у них не развиты и врядли для столь узких ниш кто-то этим будет заморачиваться.
В третьих пишут их не профессиональные программисты, а специалисты в своих предметных областях.
Tags:

DT не там хотят применять (и видимо преуспеют - в виде refined types это imho скоро будет мейнстримом) - а в разработке mission critical систем - которые как раз не большие и не слишком сложные - а вот издержки там не "3-4 раза" уже сейчас - а хорошо если 30-40 - со всеми процедурами контроля качества и сертификации.

Потому там любые средства дающие допгарантии и хотя бы частичную верификацию именно экономят силы и средства.

Ну там тоже можно - F*, как оказалось, умеет проносить условия. Т.е. вы пишете
условный цЫкл сообщений, а каждую вызываемую из него функцию верхнего уровня
делаете Tot хрень. (вызываемые же из них будут автопроверяться на Тот

module IsPositive

let is_positive i = i > 0

val is_double_positive : int -> Tot bool
let is_double_positive i = is_positive (i+i)

Хотя ему для практики не хватат перегрузки функций. :-( Ну и с плавучкой я
вообще не понимаю, что там происходит.

Edited at 2016-07-06 11:38 pm (UTC)

Это не там придумано точно (в ATS тоже так же) - F* интересен именно тем что на нем вполне удобно писать.

В действительности я думаю туда скоро еще начнут всовывать не только тотальность - но и ограничения по расходу ресурсов (стека, памяти, сложности) - что в именно mission critical надо.

1. Это очевидная штука - без проноса код раздувается раза в 3-4. Это же не int написать, и даже не std::string. ;-)

2. Ещё не вставляют ограничения по расходу ресурсов?

3. А на чём ещё, кроме F* можно писать? На F*, кмк., это не очень получится - там без перегрузки функций вы не можете иметь 2 map'а с разными типами:

val map : (a' -> Tot b') list a' -> Tot list b'

и

val map : (a' -> ML b') list a' -> ML list b'

Аналогично и с другими обобщёнными функциями. А насколько там написано в tutorial'е, никакой перегрузки ещё не сделано.

Edited at 2016-07-07 02:43 pm (UTC)

В ATS2 с чем-чем а с перегрузкой функций все ОК - что его особенно не улучшает. В Ocaml же ее нет - но на нем вполне так массово пишут.

Ну вот вы и получаете без перегрузки:

val length2: list 'a -> Tot nat
let length2 l = List.fold_left (fun len _ -> len + 1) 0 l

Computed type "Prims.nat" and effect "FStar.All.ALL" is not compatible with the annotated type "Prims.nat" effect "Tot"

Проблема в том, что в List.fold_left жёстко зашит эффект ML.

Вот цЫтата из объяснения разработчика (в письме):

List.fold_left indeed has effect ML, which explains the error message.
Unfortunately, F* does not support effect polymorphism, so definitions of
higher-order functions have to be duplicated. In the case of lists, have a
look at https://github.com/FStarLang/FStar/blob/master/ulib/FStar.List.Tot.fst
for the pure variant of things.

Согласитесь, необходимость использовать тот или иной fold_left несколько снижает полезность языка.

Ещё вопрос - чтобы с этим всем хорошо разобраться, лучше возиться с F*? Ну там вроде бы все потроха с теорией множеств сразу вываливаются, а во всяких SPARK какие-то непонятные functional contracts.

Это первое, что напрашивается. Но mission critical систем не так уж и много, особенно таких, что бы у разработчика и заказчика были ресурсы на формальную верификацию. Так что не думаю, что это будет сильно стимулировать развития данного направления.

Речь именно том, что тут применение формальных методов снижает цену QA и сертификации (еще и давая позитивный эффект по надежности) - это именно не допрасход - а статья экономии - причем и по человеко-часам (это кроме кучи ограничений еще и тотальная инспекция кода по каждому релизу с тоннами бумаг) - и политически - используя признанную систему намного проще при сертификации объяснять "почему все хорошо".

На чем собственно SPARK например живет. Или такой вообще-то вовсе ужас как SCADE

В чистом виде не нужны. Потому что _способны_ дать профит только на стадии верификации кода, но _гарантируют_ огромный просёр ресурсов при его написании.

Но можно по частям. Всё пишется на обычных типах, и только на стадии верификации они "превращаются в зависимые" путём добавления в код правил выбранной библиотечки proof assistant.

В общем нет уже - тот же F* совершенно юзабелен. Чем и интересен.

Цикл разработки всяких скриптов и конфигов очень короткий. При этом, часто отладка происходит в "боевой" среде, поскольку создание тестовой часто оказывается очень сложной. И один неудачный запуск может привести к потере данных или остановке сервиса (даже если не в продакшене, это может помешать работе других разработчиков).
По этому очень хочется, что бы верификация происходила как можно раньше, перед каждым применением.

Скрипты это exploratory. Как минимум REPL, а лучше Jupyter.

И самое выгодное в таких случаях - вложиться в автоматизацию создания песочниц.

Песочница для скрипта, который дергает десяток сервисов, получится очень сложной.

Песочницы для сервисов, не для отдельно взятого скрипта. На круг выгоднее, чем расходы от потери данных.

Ну вот у thesz поднялся вопрос, что bash - это УЖАС-УЖАС-УЖАС. Но, реально, bash не так-то просто заменить чем-то. Нужны:

а) Ленивость.
б) Параллельность (хотя бы на уровне вызова программ).

Кроме того, если вводить строгую типизацию, то нужно сделать весёлый финт ушами с кавычками. А именно, они не должны быть обязательными:

ls "-la" "/home/potan"

аля всякие Haskell Shell заебёт кого угодно.

С третьей стороны, нужно, чтобы у любого введённого снаружи объекта обязательно сохранялось строковое описание, ведь иначе не будет работать ни grep, ни sed.

И мне, кстати, все больше и больше нравится PowerShell... :-)

А где thesz этим озаботился?

> И мне, кстати, все больше и больше нравится PowerShell... :-)

Странно.

> А где thesz этим озаботился?

Последняя запись.

Более-менее полноценный ЯП (в отличие от bash), с приспособленным к CLI синтаксисом, с некоторым подобием типизации (не строкоориентирован, есть вложенные ассоциативные массивы), и, в свежих версиях, умеет работать с json и http (значительно более удобно, чем curl+jq).
Терминал надо ставить сторонний (я использую ConEmu), стандартный просто неюзабелен.
Только комплетишен, по сравнению с bash, плоховат, даже с дополнительными пакетами.

C:\Users\mpotanin> wc -l $profile
378 C:\Users\mpotanin\Documents\WindowsPowerShell\Microsoft.PowerShell_profile.ps1

> Терминал надо ставить сторонний (я использую ConEmu), стандартный просто неюзабелен.

Да там всё не ах как круто. К терминалам на современных узких мониторах нужны мозаичные WM или разворот во весь экран.

> с некоторым подобием типизации (не строкоориентирован, есть вложенные ассоциативные массивы)

Я, лично, не понимаю, как сделать нормальную типизацию в скриптовом языке общего назначения. Требования:

а) Простота.
б) Удобство.
в) Совместимость с утилитами ком. строки.
г) Максимум проверок.

Причём пункт г-е мало того, что противоречит пункту в, так ещё и противоречив внутри. Есть два сценария использования скриптов: надёжная работа и черновая. В первом случае вы делаете скрипт "на века автономного плавания", во втором случае вам посрать, что он работает не совсем правильно, главное, чтобы хоть что-то сделал.

Пример первого поведения - это типичные скрипты загрузки, пример второго - ну какой-нибудь поиск кол-ва написанных вами строк на языке Цэ (теоретически вы должны убрать комменты, но по-факту на это насрать). Или фильтрация чего-нибудь, результат которой вы просматриваете глазами.

А зачем пункт г? Т.е. он, может, и желателен, но хотя бы а-в всё ж лучше, чем вообще без типизации.

В пункте г имелся ввиду разумный максимум проверок с учётом пунктов а-в. А совсем без пункта г - это bash, который уже есть везде.

Можете радоваться - открыли и портировали на Лин.

Уже видел, радуюсь!
Только установить пока времени не было.

Кмк., это хуйня, надолго отставшая от своего времени.

С другой стороны, как вам нравится мысель использовать SML для внутрипрограммного скриптования аля Lua?

Очень нравится. А есть встраиваемый движек?

Пока нет. Наиболее перспективные варианты, кмк - это Poly/ML (свой байткод) и MosML (отнапиленный camlrun - предок ocamlrun).

Я, собственно, подумываю этим заняться.

Так а куда в скриптах зависимые типы приткнуть? Это же замедлит скорость разработки в десятки раз. Может, кто-то и согласится тратить дни вместо минут для того, чтобы снизить вероятность факапа с 0.0001% до 0.00001%, но сомнительно, что таких задач много.

Ну не в десятки. Для маленьких прорамм замедление будет не более чем в пару раз.
И вероятность факапа для скриптов довольно высокая. Я думаю порядка 30% иногда фейлятся.

> Ну не в десятки.

Это для крупных программ будет не в десятки (а может даже и с профитом будет), а для маленьких-то - у вас на 10 строк рабочего кода будет сотня "верификации". Да если честно, если нужен наджежный скрипт, то я его с ручкой и бумажкой верифицирую быстрее, чем с любыми зависимыми типами и с тем же порядком надежности.

> И вероятность факапа для скриптов довольно высокая. Я думаю порядка 30% иногда фейлятся.

Известно, что цена ошибок тем выше, чем раньше они допущены, при этом отличие может быть вплоть до порядков, а зависимые типы ловят только то, об отлове чего позаботился программист (то, что указано в спецификации). То есть зависимые типы не способствуют решению основной проблемы. Более того - если знать где соломку подложить (то есть если хорошая и правильная спецификация есть), то надежный код можно писать хоть и на динамике, особенно когда речь о скриптах - они маленькие. Это все умеют, другое дело, что мало кому не лень это делать, оттуда и появляются ваши 30%. Так что проблема элементарно решается административными средствами.
Еще нюанс - вот скажите честно, если вы, например, пишите какой-нибудь тип для записи об аккаунте, у которого есть такие поля как имя/фамилия, телефон, индекс, мыло и т.д., то вы типы полей проставите как строки/числа или по-честному на каждое поле создадите свой тип? Если первое - нафиг вам зависимые типы, вы даже систему типов джавы не в состоянии хотя бы на половину ее возможностей для верификации использовать. И если даже не вы - ну так другие 99% программистов.

Я зависимые типы вижу в районе проектирования всякого рода железа, не только компьютерного.

Хотя и компьютерного тоже - попробуй спроектировать электрическую схему с платой, с учётом температурных и (массо)габаритных ограничений, ограничений на излучение и, в завершение, в нескольких вариантах.

Там внутре систем для такого проектирования целый язык со своими связями и ограничениями, очень развесистиыми. Части плат сохраняют для повторного использования и так далее. И всё равно, разработка сложной платы это 4-9 месяцев, как повезёт.

Железо проектируют немногие. И обычно это уже опытные разработчики. И им, конечно, помощь со стороны компилятора не помешает, но пока они и так справляются. Долго и дорого, но в тиражируемых продуктах затраты размазываются на большое число покупателей.
А скрипты пишут все кому не лень и ресурсов на полноценное тестирование обычно нет. Вот здесь бы я очень хотел иметь возможность формальной проверки, но пока не сталкивался, что бы кто-то копал в этом направлении.

Да возьми https://hackage.haskell.org/package/turtle или https://hackage.haskell.org/package/shelly или другие и добавь туда ЗТ. Попробуй.

Я повторю - между идеей и железкой проходит только 9 месяцев на разработку платы. Для нетерпеливого меня достаточно долгим сроком будет пара недель.

Радикально ты это время все равно не сократишь. Будет несть месяцев вместо девяти. Приятно, но погоду не сделает.

Чем не сокращу? Зависимыми типами? На раз. В разы (то есть, >2 раз, то есть, <2-5 месяцев).

Ты просто не представляешь, насколько всё в этой индустрии запущено.

Кто бы мне за это заплатил, бляха муха.

Я всё равно собирался это сделать, поэтому можно и на слабо повестись.

Посмотрим.

Там много и нетехнических проблем - логистика, изготовление. Если у тебя нет робота, который на месте все изготовит.
Много времени будет уходить на формулировки ограничений. При этом опытные разработчики начнут ругаться, что они "быстрее бы все просто сделали", и даже не будут совсем неправы.

Но если ты за это возьмешся и у тебя найдутся небольшие понятные подзадачи, которыми ты готов поделиться, я мог бы поучаствовать. Хотя от скриптов ожидаемой пользы, IMHO, больше, твоя задача значительно интереснее ;-).

Кстати, ты это видел?
Там Verilog используется для очень перспективных задач, требующих особой надежности :-).
Учти такое применение в своей разработке...

Вопрос - там, в зависимых типах есть поддержки симметрии? Ну, что + симметричен, а - - антисимметричен?

?

Log in