1. Dimensional analysis пишется просто как некий тип, параметризованый значением вектора заданной длины (или конечного отображения, или записи, по вкусу). Обычного вектора. Для этого не нужно писать изврат на шаблонах с MPL'ем. Сообщения об ошибках типизации адекватные. Кроме того, небольшие модификации позволяют в одной программе использовать несколько различных систем единиц (СИ, СГС, МКС, МКГСС) и переводить одни в другие без боли в заднице. Полезно не только в математике, но и практически во всех остальных областях знаний. Например, в тервере позволяет не путать ковариацию с коэфф. корреляции. "Какие-то утверждение в compile-time" это "любые утверждения в compile-time без необходимости переписывать весь код заново в синтаксисе другого вычислительного контекста того же языка". Это многого стоит
( ... )
Эта мысль "Комбинаторный стиль для того и сделан, чтобы как можно реже (т.е. никогда) не менять уже готовую функцию" очень порадовала (не сарказм). Это интуитивное ощущение или она была где-то развёрнуто сформулирована?
Несущественная придирка - В случае Agda2, это так. В случае CoQ, это не так.
Более существенно то, что чем больше ты хочешь гарантий, тем больше надо писать доказательств. И всякая автоматика пока помогает не очень-то, хотя и сколько-то помогает. Буду пробовать ещё. Но как минмиум, тесты генерить совсем просто.
> а второй более практичен (классы типов там, всё такое)
Как минимум, на agda-2.3 можно имитировать классы типов. За более ранние не помню, в каком из них это появилось.
> Самый мощный из, Coq
Он не самый мощный, он наиболее развитый. И как и Agda2, в виде нечто типа "unsafe", позволяет общую рекурсию.
Вот мне интересно, почему при достаточно активном обсуждении зависимых типов никто не говорит о системах эффектов? Я знаю, пожалуй, только 2 проекта, которые их используют - DDC и Clean (причём, если я не ошибаюсь, в последнем нельзя использовать свои эффекты). При этом эффекты гораздо, гораздо проще и ближе к среднему программисту, это очень низковисящий фрукт, прямо-таки просящий его сорвать. Вывод большинства эффектов тривиален (просто распространение по графу вызовов), мгновенный профит - от предупреждений об использовании аллоцирующих функций в tight loop'е до гарантий, что функция не будет мутировать свои аргументы (примем, что иногда мутируемость, декларируемая явно, удобна).
Да, я читаю этот ЖЖ. В частности из-за него вдохновился идеей эффектов.
Мне кажется, некорректно сравнивать эти вещи. Да, эффекты можно выразить на уровне системы типов (например, монадами); однако это, всё-таки, перпендикулярные вещи. Просто ещё одна ось - язык с системой эффектов может быть хоть с зависимыми типами, хоть динамическим.
В Haskell вложение в монаду утверждает, что эффект есть. Алгебра эффектов не развита, коммутирующие монады нужно описывать явно.
В DDC соответствующая аннотация типа (из побочной системы типов) утверждает, что эффект есть. Есть алгебра эффектов.
В Coq + Ynot есть что-то, смахивающее на монаду, утверждающее, что эффект есть, и какой именно. Алгебра эффектов частично реализована в самой библиотеке и существенно может быть расширена пользователем за счёт модульности.
Чем выше желание программиста избавиться от граблей, тем ниже по этой цепочке он уйдёт.
>В DDC соответствующая аннотация типа (из побочной системы типов) утверждает, что эффект есть Думается мне, суть в том, что это не система типов. В конце концов, в случае эффектов должны быть несколько другие правила вывода эффектов - очевидно, вывод эффекта "функция мутирует свои аргументы" несколько отличается по правилам распространения эффекта от "функция делает ио". В первом случае функция, не использующая функции с эффектом мутации над своими переменными, не будет иметь этого эффекта; во втором же эффект будет в любом случае (вероятно, после dead code elimination, ну да неважно). Поэтому это перпендикулярное термам и их типам явление.
Reply
Reply
Reply
Ещё одна область, где в каких-то частях программы очень может быть полезно доказательство, это всякое параллельное.
Reply
Reply
Есть, конечно, Numeric Prelude и Awesome Prelude, но это не переписывание имеющегося кода, это вообще другие библиотеки.
Reply
Несущественная придирка -
В случае Agda2, это так.
В случае CoQ, это не так.
Более существенно то, что чем больше ты хочешь гарантий, тем больше надо писать доказательств. И всякая автоматика пока помогает не очень-то, хотя и сколько-то помогает. Буду пробовать ещё.
Но как минмиум, тесты генерить совсем просто.
> а второй более практичен (классы типов там, всё такое)
Как минимум, на agda-2.3 можно имитировать классы типов. За более ранние не помню, в каком из них это появилось.
> Самый мощный из, Coq
Он не самый мощный, он наиболее развитый.
И как и Agda2, в виде нечто типа "unsafe", позволяет общую рекурсию.
Reply
Reply
DDC обсуждался неоднократно в ЖЖ у nponeccop.
Reply
Мне кажется, некорректно сравнивать эти вещи. Да, эффекты можно выразить на уровне системы типов (например, монадами); однако это, всё-таки, перпендикулярные вещи. Просто ещё одна ось - язык с системой эффектов может быть хоть с зависимыми типами, хоть динамическим.
Reply
В Haskell вложение в монаду утверждает, что эффект есть. Алгебра эффектов не развита, коммутирующие монады нужно описывать явно.
В DDC соответствующая аннотация типа (из побочной системы типов) утверждает, что эффект есть. Есть алгебра эффектов.
В Coq + Ynot есть что-то, смахивающее на монаду, утверждающее, что эффект есть, и какой именно. Алгебра эффектов частично реализована в самой библиотеке и существенно может быть расширена пользователем за счёт модульности.
Чем выше желание программиста избавиться от граблей, тем ниже по этой цепочке он уйдёт.
Reply
Reply
Думается мне, суть в том, что это не система типов. В конце концов, в случае эффектов должны быть несколько другие правила вывода эффектов - очевидно, вывод эффекта "функция мутирует свои аргументы" несколько отличается по правилам распространения эффекта от "функция делает ио". В первом случае функция, не использующая функции с эффектом мутации над своими переменными, не будет иметь этого эффекта; во втором же эффект будет в любом случае (вероятно, после dead code elimination, ну да неважно). Поэтому это перпендикулярное термам и их типам явление.
Я тоже не гуру :)
Reply
Leave a comment