G
|&o|Size: a a a
2020 March 24
G
Пиздец, это откуда?
В
|&o|Ему же ссылку надо получить, а не
&mutG
Изменяемая сконвертируется в неизменяемую, нет?
В
Изменяемая сконвертируется в неизменяемую, нет?
Так ты не можешь дереференснуть &&mut, &mut _: ! Copy
G
assert_eq!(vec![&1, &2, &3], [&&1, &&2, &&3].into_iter().map(|&&x| x).collect::<Vec<&i32>>());
G
А два
&& потому что into_iter устарел (возвращает ссылающийся тип), дай угадаюG
assert_eq!(vec![&1, &2, &3], vec![&&1, &&2, &&3].into_iter().map(|&x| x).collect::<Vec<&i32>>());
Да
G
Но
&mut T :! CopyG
Пиздец еботня
NL
Пиздец, это откуда?
В рекламной страничке для htop: https://hisham.hm/htop/index.php?page=screenshots
G
В рекламной страничке для htop: https://hisham.hm/htop/index.php?page=screenshots
Ты Идрис пробовал, кстати?
NL
Ты Идрис пробовал, кстати?
Только презенташку для type-safe print смотрел. Установить и поиграться не пробовал.
NL
В рекламной страничке для htop: https://hisham.hm/htop/index.php?page=screenshots
У этого товарища и статейка есть годная: https://hisham.hm/2020/01/20/dynamic-type-systems-arent-even-simpler/
G
Только презенташку для type-safe print смотрел. Установить и поиграться не пробовал.
Я первые две части книги прочитал и у меня даже в теории жизнеспособность Идриса вызвала сомнение
G
Без прувера под капотом по-моему тяжко
NL
Я первые две части книги прочитал и у меня даже в теории жизнеспособность Идриса вызвала сомнение
Ну у меня тоже есть желание начать именно с F* если мне захочется поиграть с зависимыми типами.
G
В F* по-моему только зависимые типы функций, не полноценные, как в Idris, т.к. там активно применяется подход с типами с уточнением
G
А в Idris можно явно в определении типа указывать зависимые части, есть даже зависимое сопоставление с образом и зависимые кортежи