История изменений
Исправление quasimoto, (текущая версия) :
надо проверять не только тело функции, но и все функции, которые из неё вызываются
Для этого достаточно писать handler и kmalloc в разных монадах (или любых других подобных структурах), без возможности сделать lift из второй в первую. То есть достигать выполнения инвариантов не дедуктивно (написали нечто и насилуем это проверками), а индуктивно, то есть так, что сами вещи композицонно (согласно type rules) не смогут образовать expressions которые нам не нужны (содержат kmalloc в handler), по аналогии с тем как
template <typename T> struct List ...
чисто индуктивно образует гомогенный список - нам тут нужно то же самое, но на уровне не конструкторов списков, а комбинаторов последовательного выполнения (вместо semicolon), лексических биндингов переменных (можно лямбдами) и т.п.
Ну например - в хаскеле есть STM :: * -> * и IO :: * -> * и atomically :: STM a -> IO a - в монаде STM я не могу делать IO операций (точнее, могу, но это особая GHC-зависимая unsafe фича с которой нужна осторожность и за которой легко следить), могу только составить сложную транзакцию (любой чистый код, любое чтение/запись разных STM контейнеров) и кинуть её в IO. Ну и так же - я могу кинуть чистое значение в IO, но не могу вытащить обратно (опять же, без unsafe фич).
Исходная версия quasimoto, :
надо проверять не только тело функции, но и все функции, которые из неё вызываются
Для этого достаточно писать handler и kmalloc в разных монадах (или любых других подобных структурах), без возможности сделать lift из второй в первую. То есть достигать выполнения инвариантов не дедуктивно (написали нечто и насилуем это проверками), а индуктивно, то есть так, что сами вещи композицонно (согласно type rules) не смогут образовать expressions которые нам не нужны (содержат kmalloc в handler), по аналогии с тем как
template <typename T> struct List ...
чисто индуктивно образует гомогенный список - нам тут нужно то же самое, но на уровне не конструкторов списков, а комбинаторов последовательного выполнения (вместо semicolon), лексических биндингов переменных (можно лямбдами) и т.п.
Ну например - в хаскеле есть STM :: * -> * и IO :: * -> * и atomically :: STM a -> IO a - в монаде STM я не могу делать IO операций (точнее, могу, но это особая GHC-зависимая unsafe фича с которой нужна осторожность и за которой легко следить), могу только составить сложную транзакции (любой чистый код, любое чтение/запись разных STM контейнеров) и кинуть её в IO. Ну и так же - я могу кинуть чистое значение в IO, но не могу вытащить обратно (опять же, без unsafe фич).