169 похожих чатов

А зачем в кваскель тащить зависимые типы?

26 ответов

19 просмотров

Потому что завтипы это секас

Danil-Berestov Автор вопроса
Nutritional Rabbit
Потому что завтипы это секас

идрес вот с нуля не может до сих пор сделать, чтобы было _нормально_

Danil-Berestov Автор вопроса
Oleg ℕižnik
офтоп, но что ненормального то

Ну какое-то время назад говорили, что компеляция иногда просто не заканчивается, или типа того

Danil Berestov
Ну какое-то время назад говорили, что компеляция и...

Так это так в любом языке с достаточно мощной системой типов, это показатель нормальности, а не наоборот

Danil-Berestov Автор вопроса
Oleg ℕižnik
Так это так в любом языке с достаточно мощной сист...

Ну хочется всё же собирать программу за конечное время. Тоже _нормальное_ желание)

Danil Berestov
Ну хочется всё же собирать программу за конечное в...

Если все функции тотальные, то за конечное соберётся, просто за большое конечное

Danil Berestov
Ну хочется всё же собирать программу за конечное в...

Ну если хочется верхний баунд на время конпеляции, тогда нужно использовать не хаскель и не скалу

Danil Berestov
Ну хочется всё же собирать программу за конечное в...

Это же проблема сложности программ, которые позволяет писать система типов. Не причина из запрещать

Danil-Berestov Автор вопроса
Oleg ℕižnik
Ну если хочется верхний баунд на время конпеляции,...

Ну наши 130к компилируются за 3,5 минуты, например)

избавить от использования синглтонов

Danil-Berestov Автор вопроса
adam Белоочий
избавить от использования синглтонов

норм, но в синглтонах тоже пока не алё. знаю тока, шо можно классное че-то делать

Danil Berestov
Ну наши 130к компилируются за 3,5 минуты, например...

Ну если у вас есть большая программа на хаскеле, которая быстро собирается, а у кого-то есть маленькая программа на идрисе, которая долго собирается, действительно стоит сделать вывод, что дело в ЯП

Danil Berestov
Ну наши 130к компилируются за 3,5 минуты, например...

У вас там только изменённые части пересобираются что ли?

Danil Berestov
норм, но в синглтонах тоже пока не алё. знаю тока,...

Синглтоны это, конечно, круто, но область памяти без определённого времени жизни это отстой. Накидаешь ты этих сингтонов, а потребление оперы ниже 500 метров не опускается, кул, да?

Danil-Berestov Автор вопроса
Danil Berestov
всё ещё меньше холодного хрома

Ну, это я при минимальную планку, по максимуму там спейслик и минус 6 гб оперы

Oleg ℕižnik
офтоп, но что ненормального то

прокомментируйте пожалусто критику кьютити на странице 29, чет эйзенберг любит на это налегать, но мне проблема особо серьезной не кажется

Danil Berestov
расшифруеш наброс?

говорю ж на стр 29 написано, в видосе выше эйзенберг тоже про это упоминает

A64m AL256m qn<cores> I0
прокомментируйте пожалусто критику кьютити на стра...

я честно вчитался в 29, не прочитав статьи целиком там получается два минуса - первый это какие-то полукольца, у которых произведение не нулей может быть нулём и единственный пример - это какая-то странная секьюрити система типов, где я так понимаю, у вас есть вектор разрешений и если например терм c разрешением (r:1. w: 0) замещается внутри терма с разрешением (r:0, w:1) то произведение будет нулевым, и вот тут QTT и проиграла а второй минус, возможно более серьёзный с патерн-матчингом, но я пока не знаю, как правильно суммы делаются в QTT

Похожие вопросы

Обсуждают сегодня

Господа, а что сейчас вообще с рынком труда на делфи происходит? Какова ситуация?
Rꙮman Yankꙮvsky
29
А вообще, что может смущать в самой Julia - бы сказал, что нет единого стандартного подхода по многим моментам, поэтому многое выглядит как "хаки" и произвол. Короче говоря, с...
Viktor G.
2
30500 за редактор? )
Владимир
47
а через ESC-код ?
Alexey Kulakov
29
Чёт не понял, я ж правильной функцией воспользовался чтобы вывести отладочную информацию? но что-то она не ловится
notme
18
У меня есть функция где происходит это: write_bit(buffer, 1); write_bit(buffer, 0); write_bit(buffer, 1); write_bit(buffer, 1); write_bit(buffer, 1); w...
~
14
Добрый день! Скажите пожалуйста, а какие программы вы бы рекомендовали написать для того, чтобы научиться управлять памятью? Можно написать динамический массив, можно связный ...
Филипп
7
Недавно Google Project Zero нашёл багу в SQLite с помощью LLM, о чём достаточно было шумно в определённых интернетах, которые сопровождались рассказами, что скоро всех "ибешни...
Alex Sherbakov
5
Ребят в СИ можно реализовать ООП?
Николай
33
https://github.com/erlang/otp/blob/OTP-27.1/lib/kernel/src/logger_h_common.erl#L174 https://github.com/erlang/otp/blob/OTP-27.1/lib/kernel/src/logger_olp.erl#L76 15 лет назад...
Maksim Lapshin
20
Карта сайта