[Haskell] простой вопрос

> Да я твержу-твержу, что нет. Термы IO переводятся в термы target

Что еще за термы IO? Термы target - это в рассматриваемом случае и есть представление IO. То есть IO хранится в виде термов target грубо говоря.

а я показал пример семантики где IO - часть source

Ну в том и дело, что такой семантики дать нельзя, потому что нам нужна run. А у функции run семантики в хаскеле быть не может, так как самой функции run в хаскеле быть не может.

Какие конкретные преимущества это несёт по сравнению с хаскелем?

Как обычно, когда идет речь о системах типов, то преимущество бывает только одно - язык выглядит стройнее и логичнее, не нужны костыли.

> А, собственно, зачем нам run для IO?

Потому что семантика ф-и run - это _и есть_ семантика IO.

Любую хаскельную программу можно написать и без него.

Конечно, можно. Но еще раз. Любая программа на хаскеле возвращает некоторый терм target. И мы можем написать семантику вычисления этого терма. И на этом можно закончить. Но нам ведь хочется, чтобы программа делала что-то полезное - например, обрабатывала какие-то входные данные, что-то выводила. А значит, нам необходима семантика IO - то есть семантика исполнения target-кода. А это и есть функция run.

Факт того, что нельзя в языке определить функцию с типом (IO a -> a)

По факту определить ее можно, проблема в том, что это будет не функция.

эти недетерминированные значения на уровне детерминированного вычислителя появляться (run) и не должны.

См. выше. Если мы ограничиваемся семантикой самого хаскеля и семантика IO нам не нужна - то все так. Но если мы хотим дать полную операционную семантику, чтобы знать, как выполняется наша программа, то мы необходимо должны специфицировать поведение run. Но в хаскеле нету и не может быть функции run. А значит, мы не можем описать семантику IO, описывая семантику конструкций хаскеля. Семантику IO можно дать только описав target-язык.

в первом случае это просто ad-hoc запрет, а во втором - действия правил типизации.

Это существенная разница. Так же можно сказать «в динамических ЯП нам просто ad-hoc запрещают складывать слонов с бегемотами, а в статических - следит система типов».

Вот здесь: [Haskell] простой вопрос (комментарий)

Я говорю, где о чистоте шла речь в моем предыдущем посте (на который ты ответил «То есть, ты согласен, что деление на чистые и нечистые функции вполне практично?»).

А какие ещё, кроме нечистоты, имеются ограничения на применение мемоизации?

> А какие ещё, кроме нечистоты, имеются ограничения на применение мемоизации?

А нечистота и не является ограничений на применение мемоизации. Ограничением является некорректная работа программы. Если ты функция мемоизировал и программа работает правильно - то все хорошо, мемоизировать можно.

Ограничением является некорректная работа программы.

Мда. Это утверждение настолько применимо вообще к чему угодно в девелопменте, что я не понимаю, для чего у нас такой раздел.

Как применимость этого утверждения относится к предмету разговора?

Никак, как и само утверждение.

Утверждение как раз относится прямо.

Что еще за термы IO?

Подтермы Core (~ SystemF), т.е. в Core у нас есть лямбда, аппликация, переменные, case, и т.д.; также там есть конструкторы примитивных и алгебраических типов данных. Язык конструкторов данного типа данных (т.е. термы этого типа данных) - это часть Core. Архитектурное отличие (костыли?) хаскеля в том, что он некоторые конструкторы (типов IO и STM) преобразует не так как все остальные.

Ну в том и дело, что такой семантики дать нельзя, потому что нам нужна run. А у функции run семантики в хаскеле быть не может, так как самой функции run в хаскеле быть не может.

Не, чтобы дать семантику языка нужно дать его грамматику - некий тип Syntax. И затем определить либо, метациклически, eval : Syntax -> Syntax, либо, операционно, compile : Syntax -> VM. А runIO тут вообще сопряжена - она может вытаскивать значения из VM обратно.

Как обычно, когда идет речь о системах типов, то преимущество бывает только одно - язык выглядит стройнее и логичнее, не нужны костыли.

Ну, помимо effect types есть ещё 100500 сужений unrestricted системы типов, которые позволяют языку выглядеть стройнее и логичнее. Вопрос в том нужно ли их все применять при построении языка.

Потому что семантика ф-и run - это _и есть_ семантика IO.

Это семантика _выполнения_ IO в рамках target, к хаскелю, да, отношения не имееющая. Когда мы выбираем target для операционной семантики мы заведомо ему «доверяем», т.е. что термы target и вычисления правильно выполнят и эффекты нужные произведут.

Но в хаскеле нету и не может быть функции run.

Ну почему, нужно добавить ещё Heap, и конструктор New, тогда выделив Bus на Heap, поместив туда (предполагаемые недетерминированные) данные можно запустить run и получить (недетерминированный, как следствие) результат.

module IOSemantic where

open import Data.Bool
open import Data.Nat
open import Data.Fin
open import Data.List
open import Data.Product

-- | FIXME: Fin equality using stdlib?
_≡_ : ∀ {n} → Fin n → Fin n → Bool
zero    ≡ zero    = true
_       ≡ zero    = false
zero    ≡ _       = false
(suc n) ≡ (suc m) = n ≡ m

Data : Set
Data = ℕ

Index : ∀ {n} → Set
Index {n} = Fin n

Array : ℕ → Set
Array _ = Index → Data

Shape : Set
Shape = List ℕ

data Heap : Shape → Set where
  Empty   : Heap []
  Alloc   : {n : ℕ} {ns : Shape}
          → Array n → Heap ns → Heap (n ∷ ns)

data Loc  : ℕ → Shape → Set where
  Top     : {n : ℕ} {ns : Shape}
          → Loc n (n ∷ ns)
  Pop     : {n k : ℕ} {ns : Shape}
          → Loc n ns → Loc n (k ∷ ns)

data IO (a : Set) : Shape → Shape → Set where
  Return  : {ns : Shape}
          → a → IO a ns ns
  Write   : {n : ℕ} {ns ms : Shape}
          → Loc n ns → Index {n} → Data → IO a ns ms → IO a ns ms
  Read    : {n : ℕ} {ns ms : Shape}
          → Loc n ns → Index {n} → (Data → IO a ns ms) → IO a ns ms
  New     : {ns ms : Shape}
          → (n : ℕ) → (Loc n (n ∷ ns) → IO a (n ∷ ns) ms) → IO a ns ms

return : ∀ {a ns} → a → IO a ns ns
return = Return

_>>=_ : ∀ {a b ns ms ks} → IO a ns ms → (a → IO b ms ks) → IO b ns ks
Return x       >>= f = f x
Write a i x wr >>= f = Write a i x (wr >>= f)
Read a i rd    >>= f = Read a i (λ x → rd x >>= f)
New n io       >>= f = New n (λ a → io a >>= f)

lookup : ∀ {n ns} → Loc n ns → Index → Heap ns → Data
lookup Top     i (Alloc a _) = a i
lookup (Pop k) i (Alloc _ h) = lookup k i h

updateArray : ∀ {n} → Index → Data → Array n → Array n
updateArray i d a = λ j → if i ≡ j then d else a j

updateHeap : ∀ {n ns} → Loc n ns → Index → Data → Heap ns → Heap ns
updateHeap Top     i x (Alloc a h) = Alloc (updateArray i x a) h
updateHeap (Pop k) i x (Alloc a h) = Alloc a (updateHeap k i x h)

run : ∀ {a ns ms} → IO a ns ms → Heap ns → a × (Heap ms)
run (Return x)       h = x , h
run (Read a i rd)    h = run (rd (lookup a i h)) h
run (Write a i x wr) h = run wr (updateHeap a i x h)
run (New n io)       h = run (io Top) (Alloc (λ i → 0) h)

А откуда возьмутся эти недетерминированные данные, это уже совсем другой вопрос.

откуда возьмутся эти недетерминированные данные

Ну, то есть, программа которая лежит в сегменте кода это суть детерминированный control flow (представляемый определёнными инструкциями для CPU) и недетерминированные значения в него попадают автоматически (аппаратно).