Введение
Воскресное утро, время для еще одного эпизода в серии Безумные Воскресения. Еще раз в одной категории с риском разрыва мозгов, но ведь это как раз то, что нам нравится, не так ли? На этот раз мы рассмотрим бестиповое лямбда-исчисление в C#. Но погодите, разве C# не типизированный язык? Действительно. Но значит ли это, что все, что вы делаете на C# должно быть статически типизировано? Не обязательно: типизация присутствует в языке как инструмент, который вы можете либо не трогать, либо применить. В этом топике мы рассмотрим как новое ключевое слово dynamic из C# 4.0 под несколько странным углом…
Иногда типы становятся преградами на пути: может что-то изначально нетипизировано (как XML-документы без схемы, веб-сервисы без контракта WSDL, и др.) либо подразумевается, что это что-то динамически типизировано (как объекты, приходящие из динамических языков вроде Ruby или Python). И наконец пресловутые API, которые не придерживаются своих типов: в какой-то момент у вас статическая типизация, но в конце концов вы приходите к тому, что у вас System.Object везде где только можно (как взаимодействие COM библиотеками MS Office). Для всех этих случаев как раз и полагается dynamic C# 4.0. Классический пример проиллюстрировать эту особенность, рассказать об IronPython-объекте из C#. Сначала определение в Python:
class Calc:
def Add(self, a, b):
return a + b
def GetCalc():
return Calc()
* This source code was highlighted with Source Code Highlighter.Самое прекрасное в этом Python-калькуляторе, это его способность работать со всем, что поддерживает оператор сложения. Другими словами, мы можем скормить ему два целочисленных объекта или две строки, или даже DateTime и TimeSpan. Чтобы произвести эти вызовы, мы используем ключевое слово dynamic в C#:
var py = Python.CreateEngine();
dynamic script = py.ImportModule("Calc");
dynamic calc = script.GetCalc();
int three = calc.Add(1, 2);
* This source code was highlighted with Source Code Highlighter.Не обращайте внимания на несколько технических строк для загрузки файла Python; здесь самым важным является факт того, что тип переменной calc описан как dynamic, что значит все операции, вызываемые из нее, будут разрешены во время выполнения:
Я не буду вдаваться в подробности того как это работает, может в другой раз (вне тематики безумных воскресных топиков), но в этом суть данной возможности. Вместо этого, мы сделаем кое-что в стиле «не пытайтесь повторить это в домашних условиях»: введем бестиповое лямбда-исчисление.
Бестиповое лямбда-исчисление как оно есть
Бестиповое лямбда-исчисление, разработанное Алонзо Чёрчем около 1930, это теория о вычислительных аспектах функций. Она рассматривает функции как правила и определяет две дружественные операции чтобы работать с ними: абстракция и аппликация. В сущности, это все, но тем не менее, теория породила собой огромное пространство для исследований. Чтобы убедить вас в этом, предлагаю вам посмотреть в вашем любимом онлайновом книжном магазине какое количество страниц в этой книге:
(прим. переводчика: не так уж чтобы совсем много: 621 см. books.google.com.ua/books?id=ZdydJZVue50C&dq=the+lambda+calculus+its+syntax+and+semantics&hl=ru&source=gbs_navlinks_s)
Итак, позвольте мне суммировать основные вещи, цитируя/перефразируя книгу выше. Во-первых, мы должны определить концепцию λ-терма:
В качестве типичного упражнения, вынесите четвертый лямбда-терм в примерах из его полностью скобочной и раздутой формы.
Везде, где есть лямбда-термы, их можно обозначить функциями, также как это делается в C# с помощью лямбда-выражений. Например, второй пример выше является функцией с аргументом «x», которая возвращает «x». Другими словами, это тождественная функция. Однако, она не имеет типа: она может оперировать чем угодно (в частности, другими лямбда-термами). На C# мы можем написать это вот так:
Func<T, T> I = x => x;
где T означает параметр-обобщение (generic parameter). Очевидно, эта функция может оперировать значениями, но также хорошо она может оперировать функциями: принимая функцию, она вернет точно такую же функцию:
I(5) // produces 5
I(I) // produces I
Фактически, ближайшие три примера выше являются закрытыми термами, в том смысле, что все символы, используемые в их «теле функции» (часть после точки) находятся в «области действия» путем абстракции(й) над ними. Мы называем их комбинаторами:
Последний терм в предыдущем примере не закрыт: он возвращает «х», который не был абстрагирован наружу. Это отражает концепцию замыкания, которую мы имеем в C#:
R x = …;
Func<T, R> f = z => x;
Сейчас мы не будем больше углубляться в это, но достаточно сказать, что такие красивые слова как «замыкание» глубоко укоренились в теоретических основах. Считайте себя счастливчиками, что вам довелось работать с языком, возлежащим на таких солидных теоретических основаниях :-).
Далее, нам нужна концепция свободных переменных. Вкратце, она позволит нам идентифицировать те переменные, которые не введены абстракцией в данный терм. Это определение отличается предельной простотой:
Для комбинаторов набор свободных переменных будет пустым. Напротив, для нашего последнего примера (один результат в замыкании) набор будет содержать только один «x». Ничего невообразимого, правда?
И наконец, теперь мы можем определить как аппликация каррируется, на основании замещения:
Чтобы избежать пересечений имен (что формально можно предотвратить используя соглашение по именованию переменных, применив FV (свободных переменных) выше), мы будем как можно более аккуратными в именовании переменных. Все мы знаем это из C# и это просто теоретическая основа для зон видимости:
Func<T, T> I1 = x => x;
и
Func<T, T> I2 = y => y;
фактически являются «одним и тем же». Опасное дело использовать такие большие слова в контексте целой среды выполнения (CLR) и языка (C#).
Я не утверждаю что I1 и I2 ссылаются на тот же делегат: нет идентификации между делегатами, которые говорят что «x => x» и «y => y» одно и то же. Скорее, я указываю здесь на то, что окружение I1 и I2 будет одним и тем же когда применено к одному и тому же объекту. В лямбда-исчислении это осносится к альфа-преобразованиям.
Пока что игнорируя важную проблему конфликтов имен, рассмотрим поближе вышеприведенное правило «бета-преобразования». Идея проста: «аппликация абстракции с другим термом дает в результате замещение». Это почти то же самое, что и вызов делегатов в C#, но все же с некоторыми отличиями: в мире лямбда-исчислений, замещения есть ни что иное как механическое переписывание термов. В языках вроде C#, код компилируется как есть и вызов делегата не переписывает магическим образом тело делегата на лету. Но еще более важно, в C# мы оказываемся непосредственно заинтересованы в семантике вызова по значению: передвызовом, аргументы должны быть приведены к «значению», которое может быть передано в вызов (через механизм вызова делегатов).
Нетипизированное или универсально типизированное? (Untyped or uni-typed?)
А теперь вопрос сегодняшнего дня: можем ли мы типизировать (в смысле системы типов CLR/C#) все лямбда-термы? Вроде как мы уже делали это с комбинатором I, выражая его как Func<T, T> используя обобщения (дженерики): передавая значение конкретного типа T, результатом является то же самое значение и точно тот же тип. В самом деле, как насчет выведения таких сигнатур? C# не делает этого, но F# может (чероез выведение типов по Хиндли—Милнеру, как это делается обычно в ML-образных языках):
Okay, «I» выведен к типу чтобы быть типом который идет от 'a к 'a, где 'a — это нотация для обобщенного параметра. Как насчет K, комбинатора, принимающего два аргумента и всегда возвращающего первый из них (породитель «постоянного» значения):
Похоже, мы все еще неплохо продвигаемся. F# вывел тип, который должен быть "‘a к ‘b к ‘a". Вау, что здесь происходит? В C#, это будет выглядеть как Func<T1, Func<T2, T1>>: функция, которая получает аргумент типа T1 возвращает функцию, которая принимает аргумент типа T2 и возвращает значение типа T1. Врубаетесь? То, что здесь произошло, называется «карринг, когда функция с n аргументов превращается во „вложенные“ функции, которые обслуживают по одному аргументу за раз. Это означает, что мы можем написать, например, „K 5“, чтобы создать новую функцию, которая кушает оставшийся аргумент „у“ (любого типа) и всегда возвращает 5.
Даже для такого (относительно) сложного зверя как S, тип может быть выведен:
Впечатляюще? На самом деле не так уж трудно. Теперь смотрите как мы сами выведем тип из тела функции. Прежде всего, мы видим x перед двумя термами: „z“ и „(y z)“. Это значит „x“ является функцией с двумя аргументами и предполагается что она кое-что возвращает. Присвоим имена типов для этих вещей: первый аргумент „z“ получает тип 'a и результат от „(y z)“ будет тип 'b. Результат мы запишем как 'c. Другими словами, тип „x“ выведен как ’a –> ‘b –> ‘c. Далее, нам нужно вывести тип „y“, на основании нашей изначальной идентификации типа для „(y z)“ как ’b. Мы видим, что „y“ — это функция с одним аргументом, „z“. Мы уже определили тип „z“ как ‘a, так что тип „y“ принимает вид ‘a –> ‘b. И наконец, наша функция „S“ также принимает „z“ в качестве третьего аргумента, который типизирован как ‘a. Теперь если это все объединить с возвращаемым типом „x“, то получим сигнатуру, показанную выше.
Ну так, это выглядит так, как будто мы можем типизировать все лямбда термы, верно? К сожалению, нет. Вот доказательство:
Здесь я написал функцию W, которая получаемый аргумент x применяет сама к себе. Такой простой лямбда терм и нельзя найти тип для него. Присоединяйтесь ко мне в этом упражнении для мозга: W принимает один аргумент x, скажем, типа 'a. Теперь, x применяется к x. Отсюда кажется, что x — это функция с одним аргументом. Этот аргумент — x, который мы уже типизировали как 'a. Как насчет возвращаемого типа? Назовем его 'b, так что теперь мы пришли к тому, что x должен быть типа ‘a –> ‘b, который не то же самое что ‘a, как у нас было раньше: унификация не удалась.
Вот где разница между бестиповым лямбда-исчислением и типовыми вариантами (как типизированное лямбда-исчисление и обобщения и еще нечто, называемое „System F“). C#, будучи типизированным языком не позволяет нам избавиться от типов вообще, так что у нас нет возможности получить нечто „нетипизированное“. Но как насчет „универсально типизированного“ (благодаря Robert Harper): заменить все типы одним единственным типом. Можем ли мы так? Ответ: с „dynamic“ мы это можем!
dynamic W = new Func<dynamic, dynamic>(x => x(x));
К сожалению, нам фактически нужен отчасти уродливый вызов конструктора делегата, но заметьте как мы присваиваем тип „dynamic –> dynamic“ к “dynamic” слева. Другими словами, мы интерпретируем все (не функциональные значения и функциональные „объекты“) как dynamic. Код выше компилируется просто замечательно, но как же работает в теле лямбды x(x)? Что ж, во времени выполнения система будет выяснять что за тип x и будет проверять, что он может быть вызван как унарная функция. Например:
dynamic W = new Func<dynamic, dynamic>(x => x(x));
W(1);
* This source code was highlighted with Source Code Highlighter.Это явно неудачное решение. Оно соответствует „вызову функции целое 1“ с аргументом „целое 1“. Ясно, что целое значение не может быть использовано как функция (это хорошо!) так что время выполнения выдаст:
Unhandled Exception: Microsoft.CSharp.RuntimeBinder.RuntimeBinderException: Cannot invoke a non-delegate type
at CallSite.Target(Closure , CallSite , Object , Object )
at System.Dynamic.UpdateDelegates.UpdateAndExecute2[T0,T1,TRet](CallSite site, T0 arg0, T1 arg1)
at UntypedLambda.Program.b__46(Object x)
at CallSite.Target(Closure , CallSite , Object , Int32 )
at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1](CallSite site, T0 arg0, T1 arg1)
at UntypedLambda.Program.Main()
То, как это устроено внутри, находится за рамками данного топика но DLR был прав, когда счел данный вызов бессмысленным.
Как насчет такого?
var I = new Func<dynamic, dynamic>(x => x);
dynamic W = new Func<dynamic, dynamic>(x => x(x));
Console.WriteLine(W(I)(42));
* This source code was highlighted with Source Code Highlighter.
А вот так теперь работает. Передавая I в W, получаем I(I), которое сокращается (используя аппликацию или бета-преобразование) в I. Эта функция используется с аргументом 42, возвращает 42.
Вы можете догадаться что … мы собираемя универсально типизировать все наши программы, используя dynamic в этих Безумных Воскресных
топиках. Разве я когда-либо упоминал Scheme? Если нет, я сделаю это сейчас :-).
От переводчика:
На днях выйдет перевод оставшейся части топика, содержащей такие разделы:
SKI combinators
Church Booleans
Church Numerals
Going nuts - recursive functions