p
как в первом хз
Type - это подтип Type1, а Type1 - Type2, это кумулятивная вселенная называется в IdrisSize: a a a
2020 June 06
G
p
Type - это подтип Type1, а Type1 - Type2, это кумулятивная вселенная называется в Idrisфигня бесполезная*
AZ
Type - это подтип Type1, а Type1 - Type2, это кумулятивная вселенная называется в Idrisи? Я не вижу причин почему в рантайме должно что-то оставться
AZ
в чем разница между
VarArgs Int 3 и Int -> Int -> Int -> Int?p
в чем разница между
VarArgs Int 3 и Int -> Int -> Int -> Int?первое это функция
G
и? Я не вижу причин почему в рантайме должно что-то оставться
Потому что
Type - как любой другой тип. А типы могут быть из значений вычислены, которые могут во время исполнения только быть известныDB
Dollar Føølish
Нужен системный язык на завтипах
Как туземцам бусы, им выпаривают андерграунд
AZ
первое это функция
в ФП языке фунцкии и значения это одно и то же, поэтому нет
AZ
первое раскрывается во второе
G
в чем разница между
VarArgs Int 3 и Int -> Int -> Int -> Int?А если
VarArgs Int !readNumber ?DF
Как туземцам бусы, им выпаривают андерграунд
А какие альтернативы?
AZ
А если
VarArgs Int !readNumber ?readNumber не является "известным в компайл тайм значением" и мы его не рассматриваем
G
readNumber не является "известным в компайл тайм значением" и мы его не рассматриваем
Почему это не рассматриваем?
DF
Даёшь констевал для идриса
AZ
Почему это не рассматриваем?
потому что вот формулировка на которой мы сошлись: https://t.me/rust_offtopic/276629
DF
К 2050 году будет готово
G
потому что вот формулировка на которой мы сошлись: https://t.me/rust_offtopic/276629
Ну я не могу ответить, не проверял, но в теории да
DB
Dollar Føølish
А какие альтернативы?
Не знаю даже, давайте теперь после каждой написанной строки код собирать и 99% времени доказывать, а в остальное -- писать логику. Поглядим, к к чьей старости напишеися хоть одна ОС на таком языке
AZ
Ну я не могу ответить, не проверял, но в теории да
