Невыводимый комбинатор и С++14

Jan 19, 2015 13:41


Есть в комбинаторной логике (и связанных с ней областях) забавная функция, обычно обозначаемая буквой M. M-комбинатор, он же пересмешник (mockingbird), он же копирующий комбинатор, он же SII, он же (λx.xx).

Теоретикам он в первую очередь интересен тем, что (M M) = ω, омега-комбинатор, простейший способ создать рекурсию (причём, в отличие от младшего брата, совершенно бесполезную). Простым же смертным, типа меня, он может запомниться в основном тем, что «ломает» к хуям вывод типов в статически типизированных языках, причем, даже как результат промежуточных вычислений. В то же время бестиповые языки прекрасно реализуют его и с ним работают без проблем.

Поехали.

Haskell:
Prelude> let i = \x -> x Prelude> let s = \a -> \b -> \c -> ((a)(c))((b)(c)) Prelude> s i i :5:5: Occurs check: cannot construct the infinite type: t1 ~ t1 -> t Expected type: (t1 -> t) -> t1 Actual type: (t1 -> t) -> t1 -> t Relevant bindings include it :: (t1 -> t) -> t (bound at :5:1) In the second argument of ��s’, namely ��i’ In the expression: s i i Prelude> Leaving GHCi. Ouch.

Ocaml:
# let i = fun x -> x;; val i : 'a -> 'a = # let s = fun a -> fun b -> fun c -> ((a)(c))((b)(c));; val s : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = # (s)(i)(i);; File "", line 1, characters 6-9: Error: This expression has type ('a -> 'b) -> 'a -> 'b but an expression was expected of type ('a -> 'b) -> 'a The type variable 'a occurs inside 'a -> 'b # let m = (s)(i)(i);; File "", line 1, characters 14-17: Error: This expression has type ('a -> 'b) -> 'a -> 'b but an expression was expected of type ('a -> 'b) -> 'a The type variable 'a occurs inside 'a -> 'b

Python:
>>> i = lambda x:x >>> s = lambda a:lambda b:lambda c:((a)(c))((b)(c)) >>> m = (s)(i)(i) >>> (m)(i)(2) 2

Typescript без типов:
var i = x => x; var s = a => b => c => ((a)(c))((b)(c)) var m = (s)(i)(i) alert((m)(i)(2)) // 2

Вообще, если взять любой достаточно обобщённый статически типизированный язык, то у него с этой простой функцией начнутся различные проблемы. В слабо типизированных языках, типа Java или C#, можно в нужных местах «выключить» типы, сведя всё к объектам и сырым типам без генериков, иначе возникнет та же проблема (код писать не буду, слишком эти языки многословны в анонимных функциях). Но.

C++14
#define LAM(X, ...) [=](auto&& X) { return __VA_ARGS__; } int main() { auto i = LAM(x, x); auto s = LAM(a, LAM(b, LAM(c, ((a)(c))((b)(c)) ))); auto m = (s)(i)(i); std::cout << (m)(i)(2) << std::endl; // 2 } Делайте с этой информацией, что хотите.

ocaml, haskell, python, typescript, С++

Previous post Next post
Up