ИЛ
Было бы неплохо убрать unwrap для любого индекса <= vec.len(), иначе это просто .get(index) с слоем абстракции
Size: a a a
2021 May 31
r
А это уже никак. Для этого нужны dependent types. Тут фишка только в том, что можно индекс проверить один раз, а потом читать много раз без проверок индекса. Но практического смысла мало, да.
ИЛ
На выходе Index будет иметь ВЖ зависимый от вектора, а для проверки мы будем использовать ссылку на вектор. Компилятор не даст нам сделать что-либо с вектором пока у нас есть этот индекс, что равноценно простому хранению ссылки на элемент
r
Да. Я не могу представить случай, где такое использование инвариантного ВЖ было бы практически полезно. Но может у меня воображение слабое.
KR
Ну а как же этот “нашумевший” GhostCell?
r
" где такое использование..." ударение на "такое"
p
Для иммутабельного вектора
r
Там обычно оптимизатор справляется. Полезно если нужно гарантировать доступ без проверок.
A
на С++ такой ужас в порядке вещей)))
[
На спп только в кт можно
A
Я про нечитаемость) Это же хаскель?
p
Это ещё не ужас.
p
Idris.
[
Это читаемо
[
То, что ты кодишь лишь на каком-то сиподобном яп, не говорит, что всем будет неудобен мл-синтаксис
p
Справедливости ради, любые пруфы сложнее тривиальных будут нечитаемы)
A
Приходится переключаться между несколькими языками постоянно. Но к с++-сным извратам так и не смог привыкнуть.
[
Я пока до этого не дошёл.
Там нельзя декомпозировать?
Там нельзя декомпозировать?
p
Можно. Но тогда будет теряться связь между компонентами. Доказал теорему А которая нужна для теоремы Б которая нужна для теоремы В и уже забыл зачем тебе А. Математики привыкшие, им проще.