PM
Для Вас sound type system даёт какие-нибудь бенефиты?
в данный момент нет, скорее интересно чего ради затеяли дотти
Size: a a a
2019 October 01
AT
в данный момент нет, скорее интересно чего ради затеяли дотти
Dotty затеяли ради вот этого. Значит, для Вас никаких бенефитов нет просто. 😊
EM
Для Вас sound type system даёт какие-нибудь бенефиты?
Она верефицировано sound, или так, на бумажке ?)
AT
Evgenii Moiseenko
Она верефицировано sound, или так, на бумажке ?)
На Coq.
EM
На Coq.
👍👍👍
AT
В смысле, DOT верефицирована на Coq. Dotty делает lowering to DOT более высокоуровневых конструкций.
AT
А вот верифицировать, что Dotty это делает "правильно" вообще нельзя, поскольку никакой другой семантики для Scala нет. 😂
PM
Dotty затеяли ради вот этого. Значит, для Вас никаких бенефитов нет просто. 😊
Понял, благодарю
M中
А вот верифицировать, что Dotty это делает "правильно" вообще нельзя, поскольку никакой другой семантики для Scala нет. 😂
но я правильно понимаю что можно хотя бы верифицировать что lowering делается так как мы (ну не мы, они) задумали?
AT
но я правильно понимаю что можно хотя бы верифицировать что lowering делается так как мы (ну не мы, они) задумали?
Я не понял, как Вы это понимаете - можете точнее описать вопрос?
AT
Можно доказать, что результат lowering (некоторая программа на DOT) обладает некоторыми свойствами (например, sound). Но нельзя доказать, что эта программа "правильно" реализует имплиситы или ещё что-нибудь, потому что для них нет никакой другой семантики (что такое "правильные" имплиситы формально?).
M中
Можно доказать, что результат lowering (некоторая программа на DOT) обладает некоторыми свойствами (например, sound). Но нельзя доказать, что эта программа "правильно" реализует имплиситы или ещё что-нибудь, потому что для них нет никакой другой семантики (что такое "правильные" имплиситы формально?).
ага, это я просто неверно понял изначальное сообщение
теперь понятно, спасибо
теперь понятно, спасибо
SK
а напомните пожалуйста какую проблему дотти решает? быстрее компиляция? или есть ещё какие-то бенефиты?
например, из языка выкидывают higher-kinded types, заменяя их энкодингом через структурные типы (type refinements) + abstract type members
SK
через экзистенциальные типы, в общем
SK
это не только упрощает язык, но и сильно упрощает компилятор, т.к. в текущем компиляторе нужно одновременно поддерживать type parameters и упомянутую выше петрушку с abstract type members, а кода, относящегося к поддержке type parameters много и он хрупкий
SK
для программиста все остается по-старому, этих изменений снаружи не видно, но хороший кусок сложности из компилятора уходит
PM
для программиста все остается по-старому, этих изменений снаружи не видно, но хороший кусок сложности из компилятора уходит
о, благодарю 🙂
2019 October 02
AT
Thoughts on TIOBE's Language Ranking Methodology – Julia Computing
https://juliacomputing.com/blog/2019/09/16/tiobe-blog.html
https://juliacomputing.com/blog/2019/09/16/tiobe-blog.html
VK
Thoughts on TIOBE's Language Ranking Methodology – Julia Computing
https://juliacomputing.com/blog/2019/09/16/tiobe-blog.html
https://juliacomputing.com/blog/2019/09/16/tiobe-blog.html
"нам не нравится наше положение в рейтинге, поэтому ему не верим " 😊