ΑZ
завтипы убивают вывод типов, не?
нет,Ю не убивают
Size: a a a
2021 January 21
EG
В имплементации завтипы, впрочем, тоже сложные, потому что требуют тотальных функций
EG
нет,Ю не убивают
Приведи контрпример, пожалуйста
EG
В плане, язык с завтипами И рабочим выводом типов
ΑZ
Приведи контрпример, пожалуйста
так ты когда-то приводил пример "выводы типов не работают". Казалось, что нельзя писать топдекларации без типов
EG
Можно исследовательский
EG
так ты когда-то приводил пример "выводы типов не работают". Казалось, что нельзя писать топдекларации без типов
Топдекларации-то хрен с ними. В идрисе вывод типов ломается просто везде, приходится the на the писать
ΑZ
Топдекларации-то хрен с ними. В идрисе вывод типов ломается просто везде, приходится the на the писать
писал только там где тип иначе нельзя вывести, например фантомный
а
вот как раз смотрел сегодня пониланг и там можно
type Alias = Clone + Whatever + You + Wantтолько там трейты это не констрейнты, а настоящие типы с множествами значений, а комбинация типов -- пересечение множеств значений поэтому
превращается в
где & это то самое перксечение типов, значит v это переменная значение которой должно быть валидным и в трейте A, и B, и C
fn myfunc<T: A + B + C>(v: T);превращается в
fn myfunc(v: A & B & C);где & это то самое перксечение типов, значит v это переменная значение которой должно быть валидным и в трейте A, и B, и C
а
прикольно
EG
Кстати
Есть ли что-нибудь легковесное, что сожрёт JSON, который выплёвывает трейсинг, и нарисует мне красивую HTML-страничку?
Есть ли что-нибудь легковесное, что сожрёт JSON, который выплёвывает трейсинг, и нарисует мне красивую HTML-страничку?
EG
Текстовые логи это хорошо, но из-за спанов они начинают выглядеть так
Jan 20 23:06:24.445 INFO build{repo.owner="GoldsteinE" repo.name="tg-vimhelpbot" branch="master" url="https://github.com/GoldsteinE/tg-vimhelpbot" commit_hash="4269ea740af48ab09edeb55a607effcc8c2ed686"}: adm::runner::git: Cloned repo https://github.com/GoldsteinE/tg-vimhelpbot to "/srv/webhook/adm/GoldsteinE/tg-vimhelpbot/master" url="https://github.com/GoldsteinE/tg-vimhelpbot" path="/srv/webhook/adm/GoldsteinE/tg-vimhelpbot/master"r
Топдекларации-то хрен с ними. В идрисе вывод типов ломается просто везде, приходится the на the писать
Дык. Неразрешимость вывода типов - плата за выразительность системы типов. И программирование лёгким движением руки превращается в доказательство теорем.
ΑZ
red75prime
Дык. Неразрешимость вывода типов - плата за выразительность системы типов. И программирование лёгким движением руки превращается в доказательство теорем.
тебе не обязательно доказывать
ΑZ
можно юзать 5% возможностей системы типов и радоваться
ΑZ
только там трейты это не констрейнты, а настоящие типы с множествами значений, а комбинация типов -- пересечение множеств значений поэтому
превращается в
где & это то самое перксечение типов, значит v это переменная значение которой должно быть валидным и в трейте A, и B, и C
fn myfunc<T: A + B + C>(v: T);превращается в
fn myfunc(v: A & B & C);где & это то самое перксечение типов, значит v это переменная значение которой должно быть валидным и в трейте A, и B, и C
ты тайпскрипт вообще не трогал?
DS
В плане, язык с завтипами И рабочим выводом типов
Нет, потому что вывод типов не разрешим в присутствии зав типов по очевидным причинам.
Пишите типы ручками
Пишите типы ручками
NL
А можешь показать пример как?
Похоже ты прав, я не нашёл реализацию через двоичную арифметику😞 В поисках этой самой арифметики даже нашёл свои древние упражнения на препроцессоре:
https://rsdn.org/forum/etude/521222.flat#531099
Это было ещё до
https://rsdn.org/forum/etude/521222.flat#531099
Это было ещё до
Boost.PP, с тех пор в препроцессор добавили VA_ARGS, и можно теперь обойтись одним unroll, а не тремя группами макросов.r
Не проще свой препроцессор написать? С рекурсией и гигиеной
NL
red75prime
Не проще свой препроцессор написать? С рекурсией и гигиеной
Тогда можно сразу haskell брать😊