ты категорически неправ, осиль хотя бы первые 20 страниц TAPL
С чего ты взял, что я его не осилил? Любая система типов - частный случай метапрограммирования (использования хуков компилятора для автоматизации решения каких-либо задач)
и *точно* система типов делалась не под это
Какая разница под что она делалась? Любая система типов - метапрограммирование само по себе.
система типов может *реализовываться* метапрограммированием, но не является метапрограммированием
Да какая разница как она реализовывается? важно что является, по определению.
каким, епрст, метапрограммированием является система типов явы 1.0?
Программист может давать компилятору хинты для того, чтобы тот мог чекать программу на корректность (в определенных рамках) или генерить более быстрый код? Может. программист может вводить новые хинты сам? может. Соответственно, метапрограммирование (программирование компилятора и его поведения для автоматизации задач программиста) присутствует. Какого качества - вопрос ортогональный. Ты просто под метапрограммированием понимаешь кодогенерацию. Но это лишь один из юзкейсов, те же макросы не обязательно генерят код - они могут менять состояние компилятора и больше ничего не делать.
я почему-то добрый сегодня, и мягко тебе скажу, что когда что-то является чем-то всего лишь по твоему определению — это не уровень разговора
Может. программист может вводить новые хинты сам? может.
в яве 1.0 не может
язык метапрограммирования может не быть тьюринг-полным, но мы тут с тобой похоже почти пришли к согласию, что метапрограммирование начинается тогда, когда есть возможность написать функцию и вызвать ее с параметрами
т.е. когда в яве (емнип 5.0) появились дженерики, т.е. стало возможно написать свой дженерик и в свой дженерик передать нечто (имя класса), то можно обсуждать, появилось метапрограммирование или нет
а до этого никакого метапрограммирования совершенно однозначно не было, хотя система типов однозначно была
я почему-то добрый сегодня, и мягко тебе скажу, что когда что-то является чем-то всего лишь по твоему определению — это не уровень разговора
При чем тут мое определение? Речь об общепринятом определении.
в яве 1.0 не может
Это как не может? В яве 1.0 нельзя определить свой класс (он и будет хинтом)?
т.е. когда в яве (емнип 5.0) появились дженерики, т.е. стало возможно написать свой дженерик (он играет роль метафункции) и потом в свой дженерик передать параметр (т.е. имя класса), то уже можно обсуждать, появилось метапрограммирование или нет
При чем тут дженерики-то? Если ты умеешь определять новые типы, то ты умеешь программировать компилятор на выполнение определенных задач, то есть занимаешься метапрограммированием.
а до этого никакого метапрограммирования не было, хотя система типов однозначно была
Чтобы система типов не была метапрограммированием, надо запретить объявлять свои типы и запретить указывать свои типы для значений, если может быть неоднозначность инференса (каковая есть в хаскеле например). Что полиморфизма
(ад-хок и параметрического) быть не должно, это и так понятно.
язык метапрограммирования может не быть тьюринг-полным
Естестественно.
но мы тут с тобой похоже почти пришли к согласию, что метапрограммирование начинается тогда, когда есть возможность написать функцию и вызвать ее с параметрами
Имеется ввиду на компайл-тайм уровне? Нет, совсем не обязательно. Определил свой класс, указал, что переменная принадлежит этому классу - все, это уже метапрограммирование.
Определил свой класс, указал, что переменная принадлежит этому классу - все, это уже метапрограммирование.
тогда и попугайчик, который определил свою какашку и указал, что она принадлежит правому контейнеру с опилками, а не левому, тоже метапрограммированием занимается
нет чувак, ты нихрена не знаешь про типы, и совершенно тупо подгоняешь факты под свою точку зрения
я про типизацию с тобой больше не говорю, и про определения тоже
нет чувак, ты нихрена не знаешь про типы, и совершенно тупо подгоняешь факты под свою точку зрения
Я ничего не подгоняю.
я про типизацию с тобой больше не говорю, и про определения тоже
А как ты можешь говорить, если сам ничего не знаешь? Твое дело - слушать, что я говорю. Если понимать под метапрограммированием кодогенерацию, то лисповые макросы не буду метапрограммированием, что бред. А если считать лисповые макросы метапрограммированием, то придется считать метапрограммированием и определение своего класса. Иначе никак.
тогда и попугайчик, который определил свою какашку и указал, что она принадлежит правому контейнеру с опилками
Ну да. Любой макрос, шаблон и т.п. сводятся к тому, что программист определяет какашку и указывает, что она принадлежит правому контейнеру с опилками.
для шаблонов с++, скажем, это выработка понимания, что нужны концепты
для системы типов хаскеля — это, скажем, выработка понимания того, что все-таки нужны семейства типов (бугага, не прошло и 20 лет после появления шаблонов в плюсах, как они с помпой сделали что-то похожее)
Шаблоны это параметрический полиморфизм в compile time, так что сравнивать нужно
Note that adding multiple inheritance and templates was considered as early as 1982.
Sam Haradhvala from Object Design Inc. did an initial implementation of templates in 1989 that Stan Lippman extended and completed for release 3.0 in 1991.
Классы типов и концепты это ограничения на параметрически полиморфные типы (ad-hoc полиморфизм) и тут
The problems caused by template arguments not being explicitly typed and not checked in isolation from the template body were appreciated at the time of the initial template design. “The Design and Evolution of C++” [Stroustrup,1994] devotes four pages (sec 14.5) to the problem and to various ways to “constrain” template arguments. The use of “constraints functions” triggered by constructors was used in the earliest template code. They are a direct ancestor of today's constraint and concept classes and of the usage-based concept idea proposed in [Stroustrup,2003a]
In July 2009, the C++11 committee decided to remove concepts from the draft standard, as they are considered «not ready» for C++11.
Ну и нужно иметь в виду, что в случае зависимых типов всё это унифицируется обратно — достаточно зависимой стрелки (dependent product types) и первого Type из иерархии универсумов, тогда вещь вида
template <typename A, typename B, size_t size> requires Comparable<A, B>
void f(A a, B b);
превращается в обычную сигнатуру вида (concept Comparable — в обычный struct/class)
void f{A B : Type}{{_ : Comparable A B}}{size : size_t}(a : A, b : B)
~
f : (A B : Type) -> Comparable A B -> size_t -> A -> B -> void
~
f : Pi(A : Type). Pi(B : Type). Pi(_ : Comparable A B). Pi(_ : size_t). Pi(_ : A). Pi(_ : B). void
где разные виды скобок это сахар на тему указаний где стирать типы ({}), где искать и подставлять нужный инстанс из контекста ({{}}) и где простые аргументы (()), Type — класс типов (не тот, а буквально — не тип, но класс _всех_ типов), а левая часть сигнатуры связывает имена A и B которые используются в правой _зависимой_ части.
Шаблоны это параметрический полиморфизм в compile time, так что сравнивать нужно
Шаблоны - это не только параметрический, но и ad-hoc полиморфизм. При чем не только для ф-й, но и для типов, то есть это 4 разных вещи. Вот ad-hoc полиморфизм на типах в хаскеле появился только с type families. А концепты тут вообще не при делах.
Классы типов и концепты это ограничения на параметрически полиморфные типы (ad-hoc полиморфизм) и тут
Ограниченная квантификация с ad-hoc полиморфизмом никак не связана, это ортогональные вещи. В классической полиморфной типизированной лямбде с подтипированием ad-hoc полиморфизма и нетути, кстати.
Ну и нужно иметь в виду, что в случае зависимых типов всё это унифицируется обратно — достаточно зависимой стрелки (dependent product types) и первого Type из иерархии универсумов, тогда вещь вида
Кстати гигиенические макросы так тоже получаются, т.к. имеем тривиальное соответствие из термов в типы (зависимые типы, терм соответствует сам себе, если есть его представление программным объектом), функция из типов в термы - параметрически полиморфная функция, в итоге макрос (функция из терма в терм «через» типы, то есть в компайлтайме) - обычная полиморфная функция, принимающая тип-терм.
// 1
template <typename A> A id(A x) { return x; }
// 2
template <typename T> class List;
// 3
template <typename A> A op(A a, A b);
template <> int op(int a, int b) { ... }
// template <> int op(int a, double b) { ... } wrong
// ...
// 4
template <typename A>
struct Monoid {
A e();
A op(A a, A b);
};
template<>
struct Monoid<int> {
static int e() { ... }
static int op(int x, int y) { ... }
};
// forall a. Monoid a => a -> a -> a -> a
template <typename A>
A op3(A a, A b, A c)
{
typedef Monoid<A> M;
return M::op(a, M::op(b, c));
}
В последнем не хватает только ограниченной квантификации Monoid-ом в сигнатуре op3 (и тут появляется концепт концептов).
Ограниченная квантификация с ad-hoc полиморфизмом никак не связана, это ортогональные вещи.
Речь шла про ограниченную квантификацию которую дают концепты и классы типов.
В классической полиморфной типизированной лямбде с подтипированием ad-hoc полиморфизма и нетути, кстати.
Э, ну да. Но речь сначала шла про общий полиморфизм (в этой самой лямбде, тоже), потом про ограничения (уже нет) — ad-hoc-ом обозвалось только потому что в хаскеле его (ad-hoc) через ограничения классов типов делают (Bounded a => a — функция перегруженная по реализациям интерфейса Bounded).
А какой конкретно макрос не занимается кодогенерацией?
Я же говорю - лиспомакрос может ничего полезного не генерить, а просто поменять стейт лисп-машины во время вызова. Ну то есть понятное дело он вернет какой-нибудь '(begin), но это чисто заглушка.
Если понимать под метапрограммированием кодогенерацию, то лисповые макросы не буду метапрограммированием, что бред. А если считать лисповые макросы метапрограммированием, то придется считать метапрограммированием и определение своего класса. Иначе никак.
лисповые макросы могут делать кодогенерацию (а могут просто менять состояние компилятора), но я не буду придираться к твоим словам, а сразу разъясню твою ошибку
да, метапрограммирование это (скорее всего) изменение состояние компилятора, но однозначно, что не всякое изменение состояние компилятора это метапрограммирование
теперь встает вопрос, а что же тогда такое метапрограммирование?
объясняю на простом примере: чем программируемый калькулятор отличается от обычного — у него есть *программируемая* кнопка
возьмем двух юзеров — *оба* изменяют внутреннее состояние калькулятора, тыкая на кнопки, но один из них программированием не занимается, а другой занимается, т.к. *изменяет* значение программируемой кнопки (т.е. изменяет ту последовательность операций, что она вызовет)
точно так же программист, просто меняющий внутреннее состояние компилятора, МЕТАпрограммированием не занимается — чтобы он занялся МЕТАпрограммированием, нужна «кнопка», назначение которой он может изменить
так вот в яве 1.0 таких кнопок *нет*; там все кнопки имеют *фиксированное* значение, и невозможно определить кнопку со своим значением
как могла бы выглядеть «программируемая кнопка» в яве? например, это могло бы быть ключевое слово struct, которое изначально ничего не делает, но которое маша может заМЕТАпрограммировать на то, что struct создает класс, у которого все поля и методы публичны, а петя может заМЕТАпрограммировать struct на то, что struct создает класс, у которого все поля обязаны быть потомком класса Widget (это чтобы формошлепщики случайно не сунули в свой struct че-то, отличное от Widget-ов)
шаблоны, кстати, тоже позволяют делать свои программируемые кнопки (хотя и не такие, как я описал), насчет дженериков явы — это вопрос
и во-вторых, перестань путать фичу с ее реализацией — т.е. типизацию с ее возможной реализацией макросами — ибо она может реализовываться не только макросами, но и кодом внутри компилятора
объясняю на простом примере: чем программируемый калькулятор отличается от обычного — у него есть *программируемая* кнопка
Ну да. Я же именно поэтому уточнил - если мы свои типы определять не можем, то метапрограммирования тут нет. А если можем - то есть, т.к. мы программируем поведение компилятора, определяем новые хинты для него со своим, уникальным поведением. Так же как кнопку для калькулятора.
но один из них программированием не занимается, а другой занимается, т.к. *изменяет* значение программируемой кнопки (т.е. изменяет ту последовательность операций, что она вызовет)
Именно. Вот именно этим и занимается джава-программист, определяя класс. Он определяет для компилятора значение некоторой лексемы (кнопки в случае калькулятора). Да, джава-программист весьма в данном случае ограничен в выразительности системы - у него достаточно мало примитивов и средств их композиции. Но их и у калькулятора не так много.
так вот в яве 1.0 таких кнопок *нет*; там все кнопки имеют *фиксированное* значение, и невозможно определить кнопку со своим значением
Нет, каждый класс и является такой кнопкой, значение которой программист меняет. Изначально эта кнопка значения не имеет, но мы его вносим. Класс задает поведение компилятора при анализе переменных соответствующего класса. Задавая класс, мы задаем поведение компилятора, то есть программируем компилятор. Проблема тут единственно в том, что эта система программирования весьма необычна и весьма далека для тьюринг-полноты (то, что она есть, не обсуждается - это факт). Так что наш спор сводится к тому, какие системы программирования на уровне компиляции считать метапрограммированием, а какие не считать. Я считаю, что считать надо все. Если ты считаешь по-другому - предлажи какие-то свое критерии. Ну можно было бы взять тьюринг-полноту, например, но многие системы типов один фиг тьюринг-полны, а макросы, с другой стороны, тьюринг-полнотой обладать совсем не обязаны.
и во-вторых, перестань путать фичу с ее реализацией — т.е. типизацию с ее возможной реализацией макросами — ибо она может реализовываться не только макросами, но и кодом внутри компилятора
Да при чем тут реализация? Я о ней вообще нигде не говорил. Это как раз ты путаешь - для тебя метапрограммирование это то, что реализовано за счет кодогенерации. В результате у тебя один и тот же концепт (шаблоны плюсов и генерики джавы) сперва метапрограммирование (в плюсах) а вот в джаве уже внезапно не факт.
Я же именно поэтому уточнил - если мы свои типы определять не можем, то метапрограммирования тут нет. А если можем - то есть,
неверно
вот тебе на память: программист определяет функции и классы, метапрограммист — метафункции и метаклассы
определение лексемы struct в моем примере это именно определение метакласса, но ты его не осилил, похоже
определение своих (непараметризованных!) типов все еще относится к программированию, а не МЕТАпрограммированию — а определение своих непараметризованных типов это просто изменение состояния компилятора
для кого, епрст, я выделял МЕТА большими буквами? а ты до сих пор путаешь программиста и МЕТАпрограммиста
о метапрограммировании в язычке типа явы речь может идти только тогда, когда типы начнут принимать параметры, и даже после этого вопрос все еще открыт
если для лисперов-схемеров создание непараметризованного типа это уже метапрограммирование — мне остается только посочувствовать то ли их невежеству, то ли бедности их языка
Задавая класс, мы задаем поведение компилятора, то есть программируем компилятор.
задавая число 1.2345, мы задаем поведение калькулятора, то есть программируем калькулятор
facepalm.jpg
чувак, в разговоре с тобой была польза в том, что я лично для себя до некоторой степени прояснил, что можно считать программированием на не тьюринг-полном языке, а что нельзя
но дальше вести с тобой разговор про метапрограммирование бесполезно
короче, давай ссылу на пейпер с новой фичей гигиены в 2013, или честно признай, что трепался
Это как раз ты путаешь - для тебя метапрограммирование это то, что реализовано за счет кодогенерации.
нет, 1. я не путаю, 2. я так не считаю — я уже писал, что в нулевом приближении метапрограммирование для меня это создание параметризованных объектов времени компиляции, а в первом приближении — эти объекты должы обрабатывать свои параметры на достаточно мощном языке (т.е. языке, близком к тьюринг-полному)
а вот то, что ты не читаешь то, что я пишу, да еще и считаешь при этом меня идиотом говорит о крайне низких твоих умственных способностях
или, как вариант, ты решил меня искусно потроллить, изображая человека с охрененной, просто выдающейся тупизной
Это как раз ты путаешь - для тебя метапрограммирование это то, что реализовано за счет кодогенерации. В результате у тебя один и тот же концепт (шаблоны плюсов и генерики джавы) сперва метапрограммирование (в плюсах) а вот в джаве уже внезапно не факт.
тройной фейспальм
вовсе не поэтому, а потому, что «метапрограммируемость», предоставляемая дженериками, сравнима с «программируемым» калькулятором, у которого на «программируемую» кнопку можно подвесить последовательность пересылок чисел между регистрами, но нельзя подвесить ни одной реальной операции (такой, как скажем сумма чисел в двух регистрах)
можно ли назвать удобство использования такой вот вычислительной *немощи* «программируемостью» — вопрос открытый
в отличие от плюсов, где кое-какие операции можно делать
вот тебе на память: программист определяет функции и классы, метапрограммист —метафункции и метаклассы
Класс это и есть метафункция. Еще раз, я рассуждаю в соответствии с определением «метапрограммирование - программирование компилятора». В соответствии с этим определением объявление класса - метапрограммирлвание. Какое определение используешь ты?
Макрос - это обычная функция, вполне времени рантайма. Просто есть возможность ее вызова во время компиляци. Алсо, а тип - это объект времени чего? Особенно если учесть тот факт что без иньроспекции типы только во время компиляции и существуют?
да, но чтобы задать семантику класса, не нужно быть МЕТАпрограммистом —достаточно быть просто программистом
А чтобы знатт семантику макросв тоже метапрограммистом быть. не надо. И давай ты уже все таки предложишь свое четко опредеение метапрограммирование, а то иначе получаются сепульки: метапрограммирование - то, чем занимается метапрограммист, метапрограммист - тот, кто занимается метапрограммированием. Если считать метапрограммированием возможность опоеделять объекты времени компиляции, то типы - метапрограммирование.
можем, вот я могу например задать 1.2345 или 4.3512, или другое число —любое значение в рамках помещающегося в регистре
Мы это число просто можем указать, но не можем описать, что оно значит, и как калькулятор долен с ним работать. Мы не можем определять новые числа, только использовать те, что определены изначально. А с типом - можем.
А в лямбда-исчислении вообще нету никаких операций. И в машине тьюринга. То естб в твоем понимании это программированием назвать нельзя. При этом это тьюринг-полные системы
Потому что ты сказал про «перспективную область исследований» — в таких случаях, помимо общего фона, обычно существуют исследовательские программы, выделяются гранты и пишутся пейперы, тезисы и книжки (например, на тему genericity со стороны типов — http://dreixel.net/research/pdf/thesis.pdf).
Чтобы решить что семейства типов нужны не надо ничего из вышеперечисденного, достаточно минимальной крупицы здравого смысла. и то что с этим так долго тянули как бы показывает всю ценность таких резулььатлв и исследований - они нужны для распила грантов и написания диссеров. Действительно, изложить в статье кучу тривиальностей значительно проще чем заниматься серьезным делом.
Тут проблема вообще в следующем - специалиты по CS идейно математики, хотя они обслуживают чисто инженерную дисциплину и должны быть физиками. Если у физика теория реальности не соответствует, то физик ее выкидывает или пытается доработаьб, у математика такого критерия нет. Математики занимаются исключительно тем, чем хотят. Вот ты можешь представить как инженер приходит к какому-нибцдь специалиту по сопромату, просит помочь в проектировании моста, а тот в ответ говорит, что инженер все делает неправильно, есть замечательная и красивая теортя атт, и инженеру надо всего лишь найти абсолютно твердые материалы и все будет хорошо? А вот в случае CS/программирования это стандартная ситуация. Подавляющее большинство занимается бирюльками вместо того, чтобы решать задачи. По тому что решение задач - это труд, а зачем прикладывать усилия, если можно не прикладывать?
Ну и как результат полная стагнация - ничего новог за 50 лет, ни одного самого замшелого результата. А и зачем? Можно же взять обычную перегрузку, известную изпокон веков, назвать подоугому, объявить рокетсаенсом - и вперед на распил грантов и защиту диссеров.
Или вот еще - придумать новую модель для логики (которых и так жопой жуй, так что ценность ее одной равна примерно нулю) и выдать это дело за новые уни блять валентные основания математики. хотя ни с новизной ни с основаниями это никак не связано. Не говоря уж о практическом применении - теорря формальных систем относится к остальной математике примерно так же как собака к каравану. Ну то есть 99% математиков совершенно наплевать что тварится в этом гетто.
Чтобы решить что семейства типов нужны не надо ничего из вышеперечисденного
То был _один_ пример (там, конечно, ничего кроме «семейства типов нужны» прописью на over 100 страниц нет :)). Это же не значит, что всё вышеперечисленное в «перспективной (?) области исследования» (системы и теории типов) существует ради конкретной этой работы — есть другие вещи.
и то что с этим так долго тянули
В смысле? Публиковали на эту тему ещё в 90-ые. В GHC было реализовано (тыц :)), так что теперь любая кухарка может, например, получить сериализацию/десериализацию (и оба ser . des = id{ByteString}, des . ser = id{Type}, автоматом) ADT for free из коробки.
изложить в статье кучу тривиальностей значительно проще чем заниматься серьезным делом.
Ну вот и где это серьёзное дело — ок, так не годится, а как нужно? Где правильный пейпер/дисер/книжка/whatever про макросы которые полезнее систем типов и грант не для распила? Или тут просто всё и так «очевидно»? Но тогда о каких исследованиях речь.
Вообще да, ты начал глубоко копать :) То есть, ты считаешь, проблема уже масштаба всего современного CS и современных pure math кафедр. Тогда paper спрашивать, действительно, нет смысла.
Это же не значит, что всё вышеперечисленное в «перспективной (?) области исследования» (системы и теории типов) существует ради конкретной этой работы —есть другие вещи.
Так все осиальное на том же уровне - устаревшие банальности и тривиальщина.
Да нет, чистая математика, конечно же, нужна (как и теоретическая физика например). И чистый CS, наверное, тоже нужен. Проблема в том, что прикладная часть CS практически не представлена. То есть вот нечто что для программистов было бы тем же, чем сопромат и т.п. дисциплины для инженера. Но этим по сути не занииается никто. Отсутствует связующее звено.
А нету их по почти, этих правильных пейперов, о том и речь. Перспективая область исследований - это не когда есть куча пейперов, а когда есть куда копать и ощутим профит от раскопок. Вот в случае тех же макросов - копать можно много куда, тк тема малоиследована, при этом дает кучу праутических профитлв в отличии от тех же типов. но проблема в чем? С точки зрения CS-теоретиков макросы это слишком сложно, не полцчается подобрать красивую теорию для описания, вообще мало теоретического бекграунда в этой области, куча неразрешенных вопросов, множество чисто технических проблем. И никто с такими сложностями связыватлся не хочат - идут по простому пути и дрочат на типы, где все уже изучено и все вопросы закрытв пол века назад.
Ну вот унивалентность и HoTT это чистая математика (Воеводский и Аводей — они кто?), просто оно связано с MLTT, то связанно с CS, а также с ПО которое используется в model checking-е, то есть уже в инженерии. Разговоры о HoTT в контексте CS при этом, конечно, чисто ради хохмы.
ЭТо не просто чистая математика - это основания математики, то есть та часть математики, на которую всем плевать, так же как программисту который пишутна яву плеват в какой там машкод у него что генерится. Еслиговорить конкретно о hott, мне и в контекте основантй польза не совсем ясна. Ну дали еще одну интерпретациб логике, в чем прорыв то? ЭТо же всем понятно что у аксиоматической теории может быть много интерпретаций. Тем более что соответствте с существующими интерпретациями тривиально, то есть безсодкржателно. Даже содержательные интерпретации (типа нестандартного анализа) особой пользы не поинесли ну а тут в чем прорыв то?
Я думаю, что любой, чей кругозор ограничивается C, OCaml, C++, Haskell, C#, Coq, Java, Epigram, Scala, Agda (гы-гы) услышав, что системы и теории типов это прошлый век, а за гигиеническими макросами PLTScheme/Racket — будущее, будет удивлён и начнёт любопытствовать — как так. Так что, чтобы удовлетворить это любопытство, — нужна либо литература, либо указания на то как вообще могло сформироваться такое мнение, либо какие-то примеры кода/задач с разбором. Потому как основания систем и теорий типов и видны в математике, и фундаментальны, и понятны (в том числе в случае динамически типизированных языков, у которых вполне хорошая теоретико-типовая семантика, в рефлексивных доменах-типах).
макросы это слишком сложно
А макросы — просто, чисто инструментарно и технично относительно реализации ЯП. Я не знаю как можно в них что-то особое найти. Ну, то есть, ты можешь делать в них всё что можешь делать в любом компиляторе (в том числе любой язык и любую систему типов для него встраивать), такой compiler pattern встроенный в язык, но всё что угодно это ничего — обычно нужно что-то конкретное (та же система типов или другие языковые фичи) и уже готовое, изученное, проверенное, оттестированное и аккуратно приготовленное в реализации языка (если речь про вещи уровня системы типов основного языка, а не какие-то микро-DSL-и).
Так все осиальное на том же уровне - устаревшие банальности и тривиальщина.
А зависимые типы — банальность и тривиальщина 40-ей давности? Тем не менее, оно развивается и уже работает (как пруф-чекеры, как минимум).
Или, например, generics (про которые те два тезиса) работают — чтобы сделать свой «msgpack» в хаскеле можно положиться на автоматические deriving и instance (Generic строит модель типа на суммах/произведениях — Binary её использует):
{-# LANGUAGE DeriveGeneric, OverloadedStrings #-}
import Data.Binary
import Data.ByteString
import GHC.Generics
data Msg
= Fix !Int
| Flt !Double
| Str !ByteString
| Arr ![Msg]
deriving (Show, Eq, Generic)
instance Binary Msg
msg = Arr [Fix (2 ^ 63 - 1), Flt 1e73, Str "1234567890"]
en = encode msg
-- Data.ByteString.Lazy.length en == 63
de = decode en :: Msg
t1 = msg == de
