s
arr i = arr (i `mod` (len arr))Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 14
K
Да это ж UB
Карлссон.жпег
Карлссон.жпег
DK
как-то туманно «(волшебный) способ…»))
именно программ, а не языков?
именно программ, а не языков?
ЗП
Зигохистоморфный Пре... in Типы в языках программирования, моделирования, представления знаний и жизни
вот изврат на пурсе
data Nat
foreign import data Zero :: Nat
foreign import data Succ :: Nat -> Nat
newtype Vec (n :: Nat) (a :: Type) = Vec (forall (u :: Nat -> Type -> Type). u Zero a -> (forall (k :: Nat). a -> u k a -> u (Succ k) a) -> u n a)
K
А теперь через Fin
DK
вот этот момент и интересен. можно ли отделить типы от (базового/несущего) языка?
gо
программ, конечно.
самое простое свойство, которое может нас интересовать это «байты памяти всегда интерпретируются тем же способом, которым интерпретировались ранее»
самое простое свойство, которое может нас интересовать это «байты памяти всегда интерпретируются тем же способом, которым интерпретировались ранее»
s
Смотри, как поворот массива получается:
↕️5
⟨ 0 1 2 3 4 ⟩
2+↕️5
⟨ 2 3 4 5 6 ⟩
5|2+↕️5
⟨ 2 3 4 0 1 ⟩
(5|2+↕️5)⊏"abcde"
"cdeab"
ЗП
Зигохистоморфный Пре... in Типы в языках программирования, моделирования, представления знаний и жизни
у пурсы нет гадтов, прийдется через лейбница записывать
gо
а дальше всё зависит от воображения
ЗП
Зигохистоморфный Пре... in Типы в языках программирования, моделирования, представления знаний и жизни
как на хаскель через фин?
gо
идрис, например, умеет отличать программы, в которых нет out-of-bounds доступа к вектору
K
Я всё пытаюсь уехать шины поменять, пни меня через 2 часа
gо
Rust умеет* отличать программы, в которых нет несинхронизированного доступа к памяти
K
* отличать
cannot be dereferenced
cannot be dereferenced
s
Вместо того, чтобы тащить пруф отсутствия out-of-bounds, можно определить функцию, которая просто всегда работает.
s
И затем доказывать отсутствие out-of-bounds отдельно, если очень надо.
K
Ага, только она UB 95% случаев и Воронеж бомбит