/pr/ – programming


c91c8c91c8a32a9724c14b89b606fd17276ec – ``Effect systems''

@8a0ed56a28c1446cbf8e8abe5cffb711 Anonymous 2017-07-26 01:28:37
Решил разобраться, что такое (algebraic) effects.
Основная идея состоит в том, что любое impure поведение может быть описано эффектом - набором примитивных impure операций, семантика которых задается обработчиками эффектов. Например, IO командной строки может быть описано двумя операциями: readline - чтение пользовательского ввода и printline - вывод строки в консоль. Для мутабельных данных это операции get и set. Для исключений - raise.
Используя синтаксис языка
@d0d99f2623594b60943fcb07120adbd8 Anonymous 2017-07-26 01:28:37
koka для определения эффектов, вышесказанное можно выразить следующим образом:
@8c400c514c354f61a8344b60a157e86e Anonymous 2017-07-26 01:29:47
effect console_io {
    readline() : string;
    printline(s : string) : ()
}

effect state<s> {
    get() : s;
    set(x : s) : ()
}

effect exception {
    raise(s : string) : a
}

Все функции в языке с эффектами имеют тип t -> e t', означающий, что функция берет на вход аргумент типа t и возвращает результат типа t' и может иметь эффект e. Функции без эффектов имеют тип t -> <> t'. Таким образом, например, операция raise эффекта exception имеет тип forall<a> string -> exception a.
@07218bca1a494b2b8804ff8cc1ac37ec Anonymous 2017-07-27 01:39:14
Композиция выражений с типами e t и t -> e' t' дает выражение с типом <e,e'> t' (почти как bind в монадах), вычисление которого уже может иметь два эффекта (точнее, скомбинированный из двух эффкетов e и e' эффект <e,e'>).
@2e57e6649b974c19958f4638416f75ee Anonymous 2017-07-27 01:39:28
Примеры:
1) readline() имеет тип console_io string и printline имеет тип string -> console_io (), значит printline(readline()) будет иметь тип console_io ();
2) get() имеет тип forall<a> state<a> a, значит printline(get()) будет иметь тип <console_io,state<string>> ().
@abd7e05612314ab28e8f109ec9e2c9d9 Anonymous 2017-07-27 01:39:59
В koka есть синтаксический сахар для таких композиций (aka do нотация в хаскелл) в виде val x = exp1; exp2. Т.е. примеры выше можно записать по-другому:
1) val x = readline(); printline(x);
2) val y = get(); printline(y).
@4ef39e4d26314a498e8ce832bc5b5d2a Anonymous 2017-07-27 01:40:34
Также еще есть очевидный синтаксический сахар для выражений (fun(x) { exp2 })(exp1), где exp2 не зависит от x, в виде exp1; exp2. Например, (fun(x) { printline("hi") })(set(123)) можно записать просто как set(123); printline("hi").
@a27397af3a59487e84189ac1125fa0e0 Anonymous 2017-07-27 01:55:40
@07218@07218bca1a494b2b8804ff8cc1ac37ec Ошибся, наоборот, не <e,e'>, а <e',e>.
@3908808e594040f887aa77b32c8d5f5a Anonymous 2017-07-27 02:01:21
(хотя, на самом деле, порядок эффектов в <> не имеет значения).
@3287bc6bc809403a8e084f6a2604252f Anonymous 2017-07-28 02:30:58
Обработчик эффекта задает интерпретацию команд эффекта и (опционально) интерпретацию финального результата. В обработчике эффекта должны быть указаны все операции (только этого) эффекта.
Пример обработчика эффекта exception:
handler { raise(s) -> count(s) }

(count вернет длину строки).
@93b9176c28c04f8798e48c84a9c4d055 Anonymous 2017-07-28 02:31:54
Такое handler выражение дает функцию, которая на вход берет action (т.е. функцию без аргументов) с эффектом exception и возможно каким-то другим эффектом e (т.е. этот action имеет тип forall<e> () -> <exception|e> int) и возвращает значение, которое имеет тип e int.
Т.е handler { raise(s) -> count(s) } имеет тип (forall<e> () -> <exception|e> int) -> e int.

Обработчик эффекта позволяет обработать этот эффект и тем самым избавиться от в него в типе.
@66c2b718c22d4c4197859087599c133a Anonymous 2017-07-28 02:32:42
По дефолту, в результате обработки эффекта, происходит остановка вычисления текущего continuation. Например,
(handler{ raise(s) -> 666 })(fun() { val x = raise("oops"); x/6 })
вернет 666 вместо 111.
@99d9bb1c42864a199746d74c37430c46 Anonymous 2017-07-28 02:33:32
Чтобы продолжить вычисление, в интерпретации (справа от -> в handler) можно использовать функцию resume, которая и есть текущая continuation. Например,
(handler{ raise(s) -> resume(666) })(fun() { val x = raise("oops"); x/6 })
вернет 111 вместо 666.
@40997e0db1fc46068d57498e7d1b87c7 Anonymous 2017-07-28 02:35:03
Чтобы обработать финальный результат (когда эффекта на самом деле не произошло в результате вычисления) используется return. Например,
выражение
if (False) then raise("oops") else 111

имеет тип exception int несмотря на то, что в результате его вычисления exception никогда не произодет и поэтому
(handler{
    raise(s) -> 666;
    return x -> x+265
})(fun() { if (False) then raise("oops") else 111 })
вернет 376.
@117bdb5906164eca9e52ec710de90d68 Anonymous 2017-07-28 02:35:29
Еще один пример. Т.к. <> это тоже формально (пустой) эффект, то для него можно создать обработчик, но т.к. операций у <> нету и всегда есть финальный результат, то он должен содержать return. Например, handler{ return x -> x }.
@93992fed144444559c0d8536a7836fa3 Anonymous 2017-07-28 02:37:28
@3287b@3287bc6bc809403a8e084f6a2604252f "команд" в смысле "операций".