We have found performance of the type inference engine to be adequate in most cases, although due to the quadratic complexity of constraint reduction it can blow up on large constraint sets.
Это называется Писец Эрлангу. Хотя, нет ни одной теории, которую нельзя было бы продемонстрировать на тривиальных примерах.
Не, настоящий писец не в этом. Он в том, что стипизировать обмен сообщениями они так и не осилили. Трудно их винить, ибо я сильно подозреваю, что без зависимых типов это ни фига не сделаешь. Но факт остаётся фактом. А эрланг без обмена сообщениями не интересен вообще никому.
Я, конечно, извиняюсь за вырванность из контекста, но, насколько я понимаю, это имеет отношение только к инструментам типа dialyzer, а не к Эрлангу как языку, и то только на сложных выражениях типа кучи навороченных if и раздутых монструозных модулей (что и так есть bad practice). А отсутствие нормальных типов еще ни один мейнстримный язык не привело к Песцу, скорее наоборот, к бессмысленному и беспощадному успеху.
Развитие структуры типов приводит к возникновению рефлекшен-библиотек и прочим приёмам залезания в кишки в обход "правильного пути". После чего этот ужас заполняет всё и вся.
В реальных проектах на сложных задачах я ещё никогда не видел "правильную структуру типов", которую бы реальным программистам, решающим реальные задачи, не приходилось бы объезжать на кривой козе.
Реальная задача приносит деньги. Компилятор или ось - это просто среда, в которой живут реальные задачи.
Выразительность системы типов тут не причём. Проблема в том, что ограничения, накладываемые ограниченными людьми, потом приходится с болью и слезами обходить. Не по тому, что они не выразительны, а потому, что они не правильны.
Так это очень древняя статья Марлоу. Костис Сагонас уже давно это все реализовал и это включено в Эрланг, называется dialyzer. Типизировать сообщения можно при определенной организации кода. В Эрланге как простой лямбде — это не система типов, а просто аннотации типов с типовыводом, как кложуровский core.typed. Мой проект Erlang Om заключался в добавлении исчисления над этим аннотационным языком для функций на типах /\. Думаю, если бы хотел сильно PhD, продолжил бы это.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2014-03-11 07:43 pm (UTC)Это называется Писец Эрлангу. Хотя, нет ни одной теории, которую нельзя было бы продемонстрировать на тривиальных примерах.
no subject
Date: 2014-03-11 07:45 pm (UTC)no subject
Date: 2014-03-11 10:27 pm (UTC)no subject
Date: 2014-03-12 08:26 am (UTC)no subject
Date: 2014-03-12 08:33 am (UTC)no subject
Date: 2014-03-12 08:40 am (UTC)no subject
Date: 2014-03-12 11:43 am (UTC)no subject
Date: 2014-03-12 11:52 am (UTC)no subject
Date: 2014-03-12 11:54 am (UTC)no subject
Date: 2014-03-12 12:06 pm (UTC)Какой критерий «реальности» задач? Считается ли написание компилятора, операционной системы или драйвера реальной задачей?
no subject
Date: 2014-03-12 12:09 pm (UTC)Выразительность системы типов тут не причём. Проблема в том, что ограничения, накладываемые ограниченными людьми, потом приходится с болью и слезами обходить. Не по тому, что они не выразительны, а потому, что они не правильны.
no subject
Date: 2014-03-12 04:14 am (UTC)no subject
Date: 2014-03-12 04:59 am (UTC)Костис Сагонас уже давно это все реализовал и это включено в Эрланг, называется dialyzer.
Типизировать сообщения можно при определенной организации кода.
В Эрланге как простой лямбде — это не система типов, а просто аннотации типов с типовыводом, как кложуровский core.typed.
Мой проект Erlang Om заключался в добавлении исчисления над этим аннотационным языком для функций на типах /\.
Думаю, если бы хотел сильно PhD, продолжил бы это.