KR
Так а что тебе тогда не понятно?
Size: a a a
2021 May 26
AN
вообще как оно выражается. там же инты это S S S Z. А если я считал какой то n из IO, то что оно о нём знает?
TK
В каком? Предположим, что есть фулловые конст дженерики. Тогда fn [T; N] -> [T; N - 1] можно будет без страха делать. Как минимум часть функционала этих ваших завтипов будет.
AN
что это такое? N же все равно "компайл тайм". Ну и в с++ сто лет уже есть конст темплейты.
AN
я спрашивал про то что если я хочу знать в коде что n < m то как это выразить. Поидее типа n должен быть S...S m
AN
только сколько S не известно.
AN
как оно работает.
TK
IO это эффекты, а эффекты или ещё что требуют, видимо, чтобы тьюринг полнота отсутствовала, или в компайл тайме чтоб было, сложно крч. Для идрисов всяких.
AN
ну вот в том же примере на хабре с вектором, как то работает.
TK
А там не читерят?
TK
Вроде паник или опшна
AN
блин. Так а нахер завтипы если потом опять опшин.
TK
Раз опшн, значит, гарантии идут лесом, пушто функция имеет право всегда возращать None
AN
один раз надо проверить, а потом уже пользуйся на здоровье пруфом.
TK
И вообще как-то не лягут завтипы на раст, имхо. Ансейфом можно обмануть любую систему доказательств при желании. И об альтернативной ветви никогда нельзя забывать.
AN
а кто говорит про раст
TK
Так же не лягут они адекватно на c++ и даже на хаскель в какой-то степени
AN
в хаскель сделают. туда всё тащат
KR
Ну
believeMe всегда будет, да. Это же не значит что выгоды от завтипов не будет.