Битва зависимых элиминаторов Bool TL;DR: По мотивам Issue: https://github.com/groupoid/exe/issues/7 Как вы знаете ленивость является фундаментальным свойтсвом всех (!) без исключения языков программирования, которые хотят или стремятся к тому, чтобы быть внутренними языками декартово замкнутой категории, или как говорят механизаторы — лямбда исчислением. Почему так? Чтобы закодировать условный оператор if без которого не обходится ни один язык программирования, в чистом лямбда ичсислении нам не обойтись без ленивости. Напишем энергичный оператор if для Bool типа (который как мы знаем совпадает со всеми кодировками, Church, Scott, Parigot, CPS и другими возможными, так как у его все конструкторы без параматеров, а кодировки обычно с параметрами работают). Вот наш тип Bool записаный на языке OM: $ cat @ ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool $ cat True λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True $ cat False λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False И вот жадный элиминатор eif: $ cat eif λ (A : *) → λ (X : #Bool/@) → λ (Y : A) → λ (Z : A) → X A Y Z Если мы скомпилируем его (т.е. сотрем информацию о типах), заэкстрактим в эрланг код, вытащим эрланг код и вставим в одну ветку оператор printf (io:format в эрланге), то при вызове этой функции eif у нас выполнятся обеи эти ветки. Вот пример использования оператора eif: $ cat eiff \ (X: #Bool/@) -> \ (Y: #Nat/@) -> #Bool/eif #Nat/@ X (#Nat/[+] Y (#Nat/Succ (#Nat/Succ (#Nat/Succ (#Nat/Succ (#Nat/Succ #Nat/Zero)))))) (Y) Тут мы вызываем условие eiff x y = if x then y + 5 else y. Так вот если вытащить ненормализированый эрланг терм и вставить в ветку с Succ printf, то при вызове eiff c True и False будет печататься этот printf: > ch:unnat(ch:ap(eiff:eiff(),['Bool':'False'(),'Nat':'Zero'()])). EIFF 0 123> ch:unnat(ch:ap(eiff:eiff(),['Bool':'True'(),'Nat':'Zero'()])). EIFF 5 Выход к этому лежит через тип Lazy: $ cat @ \ (a: *) -> \ (x: a) -> \ (y: #Unit/@) -> x $ cat delay \ (a: *) -> \ (delay: #Unit/@ -> a) -> #Lazy/@ a $ cat force \ (a: *) -> \ (force: #Unit/@ -> a) -> a Мы переписываем наш eif на ленивый if: $ cat if λ (A : *) → λ (X : #Bool/@) → λ (Y : #Unit/@ → A) → λ (Z : #Unit/@ → A) → X (#Unit/@ → A) Y Z #Unit/Make и пример: $ cat iff \ (X: #Bool/@) -> \ (Y: #List/@ #Nat/@) -> #Bool/if #Nat/@ X (\ (l: #Unit/@) -> #List/length #Nat/@ (#List/Cons #Nat/@ #Nat/Zero (#List/Cons #Nat/@ #Nat/Zero (#List/Cons #Nat/@ #Nat/Zero (#List/Cons #Nat/@ #Nat/Zero (#List/Cons #Nat/@ #Nat/Zero (#List/Cons #Nat/@ #Nat/Zero (#List/Cons #Nat/@ (#Nat/Succ #Nat/Zero) Y)))))))) (\ (p: #Unit/@) -> #List/length #Nat/@ Y) который соотвествует iff x y = if x then list.length [0,0,0,0,0,0,1|y] else lists.length y. Скомпилируем это в эрланг: > om:extract("priv/normal/Bool"). ok Теперь вытащим из него код: > l('Bool'). {module,'Bool'} > {ok,{_,[{abstract_code,{_,AC9}}]}} = beam_lib:chunks("ebin/Bool.beam",[abstract_code]). ok > io:fwrite("~s~n", [erl_prettypr:format(erl_syntax:form_list(AC9))]). Находит там функцию iff и сохраняем в файл iff.erl. Вставляем в ветке с Cons io:format("IFF!~n"), и проверяем: > ch:unnat(ch:ap(iff:iff(),['Bool':'True'(),'List':'Nil'()])). IFF! 7 11> ch:unnat(ch:ap(iff:iff(),['Bool':'False'(),'List':'Nil'()])). 0 Напоминаю что все происходило с выключенной нормализацией в om_extract: extract(F,om:fst(om:erase(om:snd(om:parse(om:read(X++"/"++F))))),1) если включить нормализацию: extract(F,om:fst(om:erase(om:normal(om:snd(om:parse(om:read(X++"/"++F)))))),1) то даже (!) c Eager IF все работает как нада (т.е. заходит в одну ветку), опускаю подробности публикую Матрицу: Norm Lazy Cnt ==== ==== ==== + + 1 + - 1 - + 1 - - 2 (unsatisfied case for runtime, two branch) Теперь смотрим как сделано в других языках: https://github.com/idris-lang/Idris-dev/blob/master/src/IRTS/Compiler.hs#L289-L303 https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/Elab/Type.hs#L232-L248 https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/Core/Unify.hs#L714-L717 https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/Core/Evaluate.hs#L123-L140 https://www.cs.ox.ac.uk/projects/utgp/school/idris-tutorial.pdf data Lazy : Type -> Type where Delay : (val : a) -> Lazy a Force : Lazy a -> a A value of type Lazy a is unevaluated until it is forced by Force. The Idris type checker knows about the Lazy type, and inserts conversions where necessary between Lazy a and a, and vice versa. We can therefore write boolCase as follows, without any explicit use of Force or Delay: boolCase : Bool -> Lazy a -> Lazy a -> a boolCase True t e = t boolCase False t e = e Т.е. сделано точно также как в Om, или другими словами через добавление обычной лямбды () -> A вместо A. Просто зашито в дешугаринге, чтобы программист сам force не писал. Вот такая петрушка. NPONECCOP патается копать глубже, но глубже у меня не получается, не вижу статей которые опровергали бы эти простые размышления и находили более глубокие подводные камни.