EG
Готовьтесь закапывать его через 30 лет
Через 30 лет, надеюсь, все будем писать на gc-free Idris 3 с линейными типами
Size: a a a
2020 June 09
G
В лишних функциях на месте критических по производительности операций. Может компилятор не соптимизировать. Или сегодня оптимизирует а завтра нет. Нельзя полагаться на это.
#[inline(always)]ЕС
#[inline(always)]И что с этим делать?
G
Через 30 лет, надеюсь, все будем писать на gc-free Idris 3 с линейными типами
+
G
И что с этим делать?
Поставить на функцию
e
Через 30 лет, надеюсь, все будем писать на gc-free Idris 3 с линейными типами
Неа
SP
В лишних функциях на месте критических по производительности операций. Может компилятор не соптимизировать. Или сегодня оптимизирует а завтра нет. Нельзя полагаться на это.
нет лишних функций
ЕС
Через 30 лет, надеюсь, все будем писать на gc-free Idris 3 с линейными типами
Нет, через 30 лет появятся только первые адекватные gc-free имплементации. Так как сейчас их нет совсем, и ресерч только начинает появляться.
ЕС
нет лишних функций
map требует в качестве аргумента функцию.
SP
не обязательно
EG
Нет, через 30 лет появятся только первые адекватные gc-free имплементации. Так как сейчас их нет совсем, и ресерч только начинает появляться.
Ну, neut уже есть, осталось написать на этой концепции нормальный язык
ЕС
Ну, neut уже есть, осталось написать на этой концепции нормальный язык
Это проба а не адекватная имплементация. Чувствуешь разницу? Точно так же как Idris 1 - проба завтипов.
EG
Ну я и сказал — осталось написать нормально
ЕС
И у gc-free очень сложный компайл-тайм, и из-за этого они компилироваться будут дольше, чем прости Господи, с++
ЕС
Ну я и сказал — осталось написать нормально
Только для этого нужно минимум 10 лет ресерча. Чтобы найти ту самую адекватную, производительную, гибкую реализацию.
ЕС
И сам Idris на самом деле не такой уж и гибкий
ЕС
Точнее он гибкий, но иногда эта гибкость требует лишней головной боли
ЕС
Как самый простой пример: попробуй сделать тип возвращаемой функции 1 or 3..10
ЕС
Придется ебаться с доказательствами и вот этим всем
ЕС
А ебаться никто не хочет, поэтому мне не особо понятно чем тебе Идрис так понравился