К вопросу о типизации
Недавний ICFPC заронил во мне тему комбинаторов в базисе SKI, и теперь хотелось бы посмотреть на неё в несколько ином ключе.
Для начала, попробуем реализовать наш базис на Хаскеле и посмотреть, что получится:
Prelude> let i x = x Prelude> let k x y = x Prelude> let s x y z = x z $ y z Попросим ghc вывести типы этих комбинаторов:
Prelude> :t i i :: t -> t Prelude> :t k k :: t -> t1 -> t Prelude> :t s s :: (t -> a -> b) -> (t -> a) -> t -> b Вроде пока всё довольно просто и очевидно. Однако, даже простейший комбинатор M, он же Mocking Bird, он же λx.x x, он же S I I из данного базиса вывести не удастся:
Prelude> let m = s i i :1:12: Occurs check: cannot construct the infinite type: a = a -> b Probable cause: `i' is applied to too few arguments In the second argument of `s', namely `i' In the expression: s i i Prelude> :t s i i :1:4: Occurs check: cannot construct the infinite type: a = a -> b Probable cause: `i' is applied to too few arguments In the second argument of `s', namely `i' In the expression: s i i Prelude> В чем же проблема? Проблема в том, что функцию λx.x x действительно нельзя протипизировать, так как её тип равен a = a -> a. Интересно, что при этом более сложные конструкции на этом комбинаторе вполне корректны:
M I = S I I I = I(I) = I Проблема здесь, очевидно, не в предпоследней редукции, она корректна и имеет тип a -> a. Проблема в том, что в этой редукции два комбинатора I суть один и тот же комбинатор! Действительно (следите за рукамиболдом), S I I I = I I (I I) = I I. Выражение I I само по себе типизируется корректно потому, что первый комбинатор инстанцируется типом (t -> t) -> t -> t, а второй (t -> t) и они прекрасно уживаются вместе. Если же это один и тот же комбинатор, то и тип у него один, и его нельзя вывести по вышеизложенным причинам. Ненавязчиво перейдём к менее функциональному языку.
public interface Function { public R invoke(A v); } Конечно, можно было бы воспользоваться какой нибудь Functional Java, но для keeping things simple лучше поизобретаем велосипед. Реализация всякой утильщины вокруг этого интерфейса довольно очевидна и не хочется на ней останавливаться, достаточно привести типы комбинаторов:
public static Function I() {...} public static Function, Function>, Function> K() {...} public static Function,Function>,Function,A0>> S() {...} Да, немного уродливо, но введённые типы статически проверяют всё, что нужно и прекрасно коррелируют с реализацией на Хаскеле (фактически, именно выведенные ghci типы и использовались, ведь в Java в роли типизатора выступает программист). Проверим работу на выражении (S (+) I 2 = 4).
Function partial = Invoker.invokeFunc2(Combiners.S(), plus, Combiners.I()); Integer res = Invoker.invokeFunc(partial, 2); // = 4 И в чем же прикол? Разумеется, вывести тип (да ещё и вручную) для M у нас снова не получится. Но мягкая статическая типизация джавы нам поможет прикинуться нетипизированной комбинаторной логикой:
Function S = Combiners.S(); Function I = Combiners.I(); // M = S I I = \x. x x Function M = (Function) Invoker.invokeFunc2(S,I,I); // M I 2 = S I I I 2 = I 2 = 2 Object mustbe2 = Invoker.invokeFunc2(M, I, 2); // = 2 Вуаля! Ну и, конечно же, имея M, почему бы и не побаловаться страшным дивергентным комбинатором Ω (= M M)?
// Omega = M M = S I I (S I I) = (\x. x x)(\x. x x) - дивергентный комбинатор Object omega = Invoker.invokeFunc(w, w); Конец немного предсказуем:
Exception in thread "main" java.lang.StackOverflowError А чего ещё хотеть от расходящегося комбинатора в языке без оптимизации хвостовой рекурсии? Разумеется, всё это ещё лучше и нагляднее бы работало в языке с «совсем» динамической типизацией, но и так заставляет задуматься: по сути, все введённые выражения можно было бы протипизировать так, чтобы корректность отличить от некорректности, или всё таки это принципиально невозможно? Можно ли операнд выражения протипизировать двумя разными типами по необходимости (или, скорее, описать такой тип, чтобы он мог вести себя по-разному в разных случаях)? В динамике (или сведённой до неё статике, как в Java) можно ввести всё, но может, есть промежуточные варианты? ...
Prelude> let i x = x Prelude> let k x y = x Prelude> let s x y z = x z $ y z Попросим ghc вывести типы этих комбинаторов:
Prelude> :t i i :: t -> t Prelude> :t k k :: t -> t1 -> t Prelude> :t s s :: (t -> a -> b) -> (t -> a) -> t -> b Вроде пока всё довольно просто и очевидно. Однако, даже простейший комбинатор M, он же Mocking Bird, он же λx.x x, он же S I I из данного базиса вывести не удастся:
Prelude> let m = s i i :1:12: Occurs check: cannot construct the infinite type: a = a -> b Probable cause: `i' is applied to too few arguments In the second argument of `s', namely `i' In the expression: s i i Prelude> :t s i i :1:4: Occurs check: cannot construct the infinite type: a = a -> b Probable cause: `i' is applied to too few arguments In the second argument of `s', namely `i' In the expression: s i i Prelude> В чем же проблема? Проблема в том, что функцию λx.x x действительно нельзя протипизировать, так как её тип равен a = a -> a. Интересно, что при этом более сложные конструкции на этом комбинаторе вполне корректны:
M I = S I I I = I(I) = I Проблема здесь, очевидно, не в предпоследней редукции, она корректна и имеет тип a -> a. Проблема в том, что в этой редукции два комбинатора I суть один и тот же комбинатор! Действительно (следите за рукамиболдом), S I I I = I I (I I) = I I. Выражение I I само по себе типизируется корректно потому, что первый комбинатор инстанцируется типом (t -> t) -> t -> t, а второй (t -> t) и они прекрасно уживаются вместе. Если же это один и тот же комбинатор, то и тип у него один, и его нельзя вывести по вышеизложенным причинам. Ненавязчиво перейдём к менее функциональному языку.
public interface Function { public R invoke(A v); } Конечно, можно было бы воспользоваться какой нибудь Functional Java, но для keeping things simple лучше поизобретаем велосипед. Реализация всякой утильщины вокруг этого интерфейса довольно очевидна и не хочется на ней останавливаться, достаточно привести типы комбинаторов:
public static Function I() {...} public static Function, Function>, Function> K() {...} public static Function,Function>,Function,A0>> S() {...} Да, немного уродливо, но введённые типы статически проверяют всё, что нужно и прекрасно коррелируют с реализацией на Хаскеле (фактически, именно выведенные ghci типы и использовались, ведь в Java в роли типизатора выступает программист). Проверим работу на выражении (S (+) I 2 = 4).
Function partial = Invoker.invokeFunc2(Combiners.S(), plus, Combiners.I()); Integer res = Invoker.invokeFunc(partial, 2); // = 4 И в чем же прикол? Разумеется, вывести тип (да ещё и вручную) для M у нас снова не получится. Но мягкая статическая типизация джавы нам поможет прикинуться нетипизированной комбинаторной логикой:
Function S = Combiners.S(); Function I = Combiners.I(); // M = S I I = \x. x x Function M = (Function) Invoker.invokeFunc2(S,I,I); // M I 2 = S I I I 2 = I 2 = 2 Object mustbe2 = Invoker.invokeFunc2(M, I, 2); // = 2 Вуаля! Ну и, конечно же, имея M, почему бы и не побаловаться страшным дивергентным комбинатором Ω (= M M)?
// Omega = M M = S I I (S I I) = (\x. x x)(\x. x x) - дивергентный комбинатор Object omega = Invoker.invokeFunc(w, w); Конец немного предсказуем:
Exception in thread "main" java.lang.StackOverflowError А чего ещё хотеть от расходящегося комбинатора в языке без оптимизации хвостовой рекурсии? Разумеется, всё это ещё лучше и нагляднее бы работало в языке с «совсем» динамической типизацией, но и так заставляет задуматься: по сути, все введённые выражения можно было бы протипизировать так, чтобы корректность отличить от некорректности, или всё таки это принципиально невозможно? Можно ли операнд выражения протипизировать двумя разными типами по необходимости (или, скорее, описать такой тип, чтобы он мог вести себя по-разному в разных случаях)? В динамике (или сведённой до неё статике, как в Java) можно ввести всё, но может, есть промежуточные варианты? ...