![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Всё, дошло
Nov. 12th, 2015 05:12 amВсё, дошло про эффекты алгебраические и коалгебраические.
Пусть есть полиморфная по эффектам функция f : {X -> Y}, и мы строим цепочку композиций
... ∘ b ∘ a ∘ f ∘ x ∘ y ∘ ...
Алгебраические эффекты это то, что поднимается по цепочке композиций вверх (то есть налево), коалгебраические — то, что прокидывается вниз.
В качестве примера алгебраического эффекта можно взять @Throws(E). Если наша функция это использует, значит что мы требуем от кого-то из caller'ов (т.е. a, или b, или может c, но на каком-то конечном уровне обязательно) хэндлер throws(e).
В качестве примера коалгебраического эффекта можно взять _@Clonable, это значит что мы требуем от нашего аргумента X, чтобы для него была задана операция clone: X -> (X, X), но не обязательно прямо: можно, чтобы для типа X и функции x : PreX -> X этого не было, но было для функции y: PrePreX -> PreX, тогда мы можем склонировать на том уровне, и применить y к каждому из результатов; можно, чтобы это было задано на ещё более далёком уровне, но где-то конечно далеко было.
Эффектные аннотации без проблем взаимодействуют с зависимыми типами, коэффектные аннотации требуют чтобы всё, от чего зависит аннотированный тип/терм, тоже было аннотировано аналогично.
Модальности удобно описывать при помощи эффектов (алгебраических, разумеется), это позволяет органично включить расширяющие логику операции в синтаксис, избегая do-нотации. Комодальности же как раз описываются при помощи коэффектов. Как описывать коэффекты алгебраически? Это мы описываем на типах какую-то структуру вместе с описанием, как она прокидывается по ним контравариантно...
Очень клёв пример пространственной гомотопической теории типов. Там задаются классическая модальность ♯, и классическая комодальность ♭.
Классическая модальность это алгебраический эффект “спросить внешнего оракула про любое утверждение P, истино оно или ложно”.
Классическая комодальность это коалгебраический эффект “потребовать, чтобы аргумент t : T шёл вместе с оракулом, умеющим отвечать на любые вопросы про его свойства P : T -> Prop”.
Пусть есть полиморфная по эффектам функция f : {X -> Y}, и мы строим цепочку композиций
... ∘ b ∘ a ∘ f ∘ x ∘ y ∘ ...
Алгебраические эффекты это то, что поднимается по цепочке композиций вверх (то есть налево), коалгебраические — то, что прокидывается вниз.
В качестве примера алгебраического эффекта можно взять @Throws(E). Если наша функция это использует, значит что мы требуем от кого-то из caller'ов (т.е. a, или b, или может c, но на каком-то конечном уровне обязательно) хэндлер throws(e).
В качестве примера коалгебраического эффекта можно взять _@Clonable, это значит что мы требуем от нашего аргумента X, чтобы для него была задана операция clone: X -> (X, X), но не обязательно прямо: можно, чтобы для типа X и функции x : PreX -> X этого не было, но было для функции y: PrePreX -> PreX, тогда мы можем склонировать на том уровне, и применить y к каждому из результатов; можно, чтобы это было задано на ещё более далёком уровне, но где-то конечно далеко было.
Эффектные аннотации без проблем взаимодействуют с зависимыми типами, коэффектные аннотации требуют чтобы всё, от чего зависит аннотированный тип/терм, тоже было аннотировано аналогично.
Модальности удобно описывать при помощи эффектов (алгебраических, разумеется), это позволяет органично включить расширяющие логику операции в синтаксис, избегая do-нотации. Комодальности же как раз описываются при помощи коэффектов. Как описывать коэффекты алгебраически? Это мы описываем на типах какую-то структуру вместе с описанием, как она прокидывается по ним контравариантно...
Очень клёв пример пространственной гомотопической теории типов. Там задаются классическая модальность ♯, и классическая комодальность ♭.
Классическая модальность это алгебраический эффект “спросить внешнего оракула про любое утверждение P, истино оно или ложно”.
Классическая комодальность это коалгебраический эффект “потребовать, чтобы аргумент t : T шёл вместе с оракулом, умеющим отвечать на любые вопросы про его свойства P : T -> Prop”.
