G
Сейчас найду
Size: a a a
2020 June 06
p
Если я пишу VarArgs Int 3 то схуяли у меня тут будут ранатйм косты?
потому что это идрис
G
Если я пишу VarArgs Int 3 то схуяли у меня тут будут ранатйм косты?
Типы могут генерироваться из значений. Значения могут быть получены во время исполнения
DF
Да, ну как бы если не устраивает то есть атс2
AZ
Типы могут генерироваться из значений. Значения могут быть получены во время исполнения
ну варарги от рантайм значений очевидно будут иметь косты, но в других япах ты просто аткое не сделаешь
DF
Там все завтипы стираются
AZ
а если ты юзаешь варарги как в расте, например, то у тебя всегда константа известная - количество аргументов
p
Dollar Føølish
Там все завтипы стираются
там их нет же
DF
Есть
G
ну варарги от рантайм значений очевидно будут иметь косты, но в других япах ты просто аткое не сделаешь
Я очень рад, что в Idris можно такое сделать, но типы-то в рантайме всё равно
G
И от них есть оверхед, иногда сильный
AZ
Я очень рад, что в Idris можно такое сделать, но типы-то в рантайме всё равно
я другое имел в виду
p
и скорее всего так и останется
AZ
окей, всё что возвращает Type и считается от компайл-тайм известных значений не имеет костов в рантайме - такая формулировка устроит?
p
я другое имел в виду
у тебя VarArgs Int 3 в общем случае раскроется в рантайме
G
окей, всё что возвращает Type и считается от компайл-тайм известных значений не имеет костов в рантайме - такая формулировка устроит?
Ну не всегда
p
окей, всё что возвращает Type и считается от компайл-тайм известных значений не имеет костов в рантайме - такая формулировка устроит?
во втором идрисе нет partial evaluation точно
p
то есть там все в рантайме