История изменений
Исправление quasimoto, (текущая версия) :
Это всё очень неправильно :)
То есть это софистика уровня «любая подпрограмма принимает одну уникальную хрень (уникальное имя аргумента f)» и «возвращает одну и ту же уникальную хрень (выражение f)» => «все подпрограммы это чистые функции из {имена аргументов} -> {тело функции}» и можно расходиться. То есть тут мы вообще к рассмотрению вопроса не подошли (что есть вещи и отображения которые моделируются типами и программами языка).
Пусть есть какой-то A : Type, _+_ : A * A -> A, f (x : A) = (x + x) : A это f : A -> A, то есть для всех a : A выражение f a (: A) в конечном итоге можно заменить на e : A (refl : Eq A (f a) e), а вот f(x : A) = (a + x) : A при мутабельном a : A это не функция, функцией снова она будет если Ref : Type -> Type, IO : Type -> Type, _+_ : Ref A * A -> IO A, a : Ref A, f(x : A) = (a + x) : IO A, f : A -> IO A, тогда для любого a : A выражение f a : IO A на e : A (... : Eq A (run (f a)) e, run : IO A -> A, semantically) не заменить.
Исходная версия quasimoto, :
Это всё очень неправильно :)
То есть это софистика уровня «любая подпрограмма принимает одну уникальную хрень (уникальное имя аргумента f)» и «возвращает одну и ту же уникальную хрень (выражение f)» => «все подпрограммы это чистые функции из {имена аргументов} -> {тело функции}» и можно расходиться. То есть тут мы вообще к рассмотрению вопроса не подошли (что есть вещи и отображения которые моделируются типами и программами языка).
Пусть есть какой-то A : Type, _+_ : A * A -> A, f (x : A) = (x + x) : A это f : A -> A, то есть для всех a : A выражение f a (: A) в конечном итоге можно заменить на e : A (refl : Id A (f a) e), а вот f(x : A) = (a + x) : A при мутабельном a : A это не функция, функцией снова она будет если Ref : Type -> Type, IO : Type -> Type, _+_ : Ref A * A -> IO A, a : Ref A, f(x : A) = (a + x) : IO A, f : A -> IO A, тогда для любого a : A выражение f a : IO A на e : A (... : Id A (run (f a)) e, run : IO A -> A, semantically) не заменить.