История изменений
Исправление quasimoto, (текущая версия) :
Для мутабельности в чистом (и, возможно, тотальном) языке «с типами» всегда достаточно монады IO и ссылок. В агде, например, это будет такой интерфейс:
IO : Set → Set
return : {A : Set} → A → IO A
bind : {A B : Set} → IO A → (A → IO B) → IO B
...
Ref : Set → Set
new : {A : Set} → A → IO (Ref A)
write : {A : Set} → Ref A → A → IO T
read : {A : Set} → Ref A → IO A
...
для него даже не нужно зависимых типов — достаточно обычного полиморфизма (по Set). И обратно — такая мутабельность не может ничего сломать в зависимых типах, если они есть, так же как она ничего не ломает в хаскеле.
Такой интерфейс суть теория (явного) IO и (явно) мутабельных (явных) ссылок (для более продвинутой теории нужно ещё навешать разных утверждений о том как все эти вещи ведут себя вместе). В качестве моделей могут выступать — 1) RTS-магия, в агде (MAlonzo) можно эти сигнатуры сделать примитивами (postulate) и перепоручить прагмами GHC (а сам хаскель делает точно так же, то есть в языке предоставляет IO и Ref-ы как абстрактные типы, оставляя всю работу RTS), вот запускаемый пример — Вышел пятый выпуск Haskell Platform (комментарий); 2) чисто языковые вещи — IDE для Haskell - когда появится? (комментарий).
Про ссылки есть глава в TAPL.
Ещё на тему семантики IO, памяти, ссылок и т.п. именно в языках с зависимыми типами — http://www.staff.science.uu.nl/~swier004/publications.html, точнее — http://www.staff.science.uu.nl/~swier004/Publications/Thesis.pdf, http://www.staff.science.uu.nl/~swier004/Publications/DepTypesForDistrArrays.pdf, http://www.staff.science.uu.nl/~swier004/Publications/MoreDepTypesForDistrArr..., http://www.staff.science.uu.nl/~swier004/Publications/HoareLogicStateMonad.pdf.
Исправление quasimoto, :
Для мутабельности в чистом (и, возможно, тотальном) языке «с типами» всегда достаточно монады IO и ссылок. В агде, например, это будет такой интерфейс:
IO : Set → Set
return : {A : Set} → A → IO A
bind : {A B : Set} → IO A → (A → IO B) → IO B
...
Ref : Set → Set
new : {A : Set} → A → IO (Ref A)
write : {A : Set} → Ref A → A → IO T
read : {A : Set} → Ref A → IO A
...
для него даже не нужно зависимых типов — достаточно обычного полиморфизма (по Set). И обратно — такая мутабельность не может ничего сломать в зависимых типах, если они есть, так же как она ничего не ломает в хаскеле.
Такой интерфейс суть теория (явного) IO и (явно) мутабельных (явных) ссылок. В качестве моделей могут выступать — 1) RTS-магия, в агде (MAlonzo) можно эти сигнатуры сделать примитивами (postulate) и перепоручить прагмами GHC (а сам хаскель делает точно так же, то есть в языке предоставляет IO и Ref-ы как абстрактные типы, оставляя всю работу RTS), вот запускаемый пример — Вышел пятый выпуск Haskell Platform (комментарий); 2) чисто языковые вещи — IDE для Haskell - когда появится? (комментарий).
Про ссылки есть глава в TAPL.
Ещё на тему семантики IO, памяти, ссылок и т.п. именно в языках с зависимыми типами — http://www.staff.science.uu.nl/~swier004/publications.html, точнее — http://www.staff.science.uu.nl/~swier004/Publications/Thesis.pdf, http://www.staff.science.uu.nl/~swier004/Publications/DepTypesForDistrArrays.pdf, http://www.staff.science.uu.nl/~swier004/Publications/MoreDepTypesForDistrArr..., http://www.staff.science.uu.nl/~swier004/Publications/HoareLogicStateMonad.pdf.
Исходная версия quasimoto, :
Для мутабельности в чистом (и, возможно, тотальном) языке «с типами» всегда достаточно монады IO и ссылок. В агде, например, это будет такой интерфейс:
IO : Set → Set
return : {A : Set} → A → IO A
_>>=_ : {A B : Set} → IO A → (A → IO B) → IO B
...
Ref : Set → Set
new : {A : Set} → A → IO (Ref A)
write : {A : Set} → Ref A → A → IO T
read : {A : Set} → Ref A → IO A
...
для него даже не нужно зависимых типов — достаточно обычного полиморфизма (по Set). И обратно — такая мутабельность не может ничего сломать в зависимых типах, если они есть, так же как она ничего не ломает в хаскеле.
Такой интерфейс суть теория (явного) IO и (явно) мутабельных (явных) ссылок. В качестве моделей могут выступать — 1) RTS-магия, в агде (MAlonzo) можно эти сигнатуры сделать примитивами (postulate) и перепоручить прагмами GHC (а сам хаскель делает точно так же, то есть в языке предоставляет IO и Ref-ы как абстрактные типы, оставляя всю работу RTS), вот запускаемый пример — Вышел пятый выпуск Haskell Platform (комментарий); 2) чисто языковые вещи — IDE для Haskell - когда появится? (комментарий).
Про ссылки есть глава в TAPL.
Ещё на тему семантики IO, памяти, ссылок и т.п. именно в языках с зависимыми типами — http://www.staff.science.uu.nl/~swier004/publications.html, точнее — http://www.staff.science.uu.nl/~swier004/Publications/Thesis.pdf, http://www.staff.science.uu.nl/~swier004/Publications/DepTypesForDistrArrays.pdf, http://www.staff.science.uu.nl/~swier004/Publications/MoreDepTypesForDistrArr..., http://www.staff.science.uu.nl/~swier004/Publications/HoareLogicStateMonad.pdf.