ЕС
извините)
Size: a a a
2020 June 24
AZ
Потому что не вижу смысла пользоваться зависимой типизацией в данном случае
"не вижу смысла пользоваться интами которые прилетают по сети, можно же оставить их строками"
AZ
Разница между списком и вектом такая же как между "12" и 12, прилетевшими по сети
G
"не вижу смысла пользоваться интами которые прилетают по сети, можно же оставить их строками"
У тебя все равно число будет
G
Что с зависимой, что нет. Если хочешь дальше вектор то сконвертируй список в вектор
AZ
zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
Вот эту функцию можно только на векторе вызватьAZ
у списка нет гарантий что зиппаются списки одной длины
AZ
как мне в этом случае быть?
G
Тогда сконвертируй в вектор возвращаемый список
AZ
можно по-разному сделать
AZ
я говорю о том что это полезно, а не "ну нахуя, в компайл атм же неизвестно"
G
Хорошо
AZ
весь смысл завтипов в том чтобы с рантайм значениями работать
r
В вектор нельзя. Можно в dependent pair или Maybe vect
AZ
с компайл тайм можно на темплейтах херачить или typenum
AZ
red75prime
В вектор нельзя. Можно в dependent pair или Maybe vect
ну там зависимая пара
DF
весь смысл завтипов в том чтобы с рантайм значениями работать
Ето ты про подход идриса говоришь. Есть ещё подход атс
DF
Где чем больше стёр тем лучше
AZ
Dollar Føølish
Где чем больше стёр тем лучше
при чем тут стер? Я про компиляцию говорю. То что после уже неинтересно
DF
Ты сказал про рантайм значкния