Время от времени люди спрашивают о реализации нетипизированного лямбда-исчисления в Haskell. [Естественно, теперь я не могу найти ни один из этих вопросов, но я уверен, что видел их!] Просто ради смеха, я решил потратить некоторое время на игру с этим.
Это достаточно тривиально, чтобы сделать что-то вроде
i = \ x -> x
k = \ x y -> x
s = \ f g x -> (f x) (g x)
Это работает отлично. Однако, как только вы попытаетесь сделать что-то вроде
s i i
средство проверки типов справедливо жалуется на бесконечный тип. По сути, все в нетипизированном лямбда-исчислении — это функции, что по существу означает, что все функции имеют бесконечную арность. Но Haskell допускает только функции конечной арности. (Потому что, действительно, зачем вам бесконечная арность?)
Что ж, оказывается, мы можем легко обойти это ограничение:
data Term = T (Term -> Term)
T f ! x = f x
i = T $ \ x -> x
k = T $ \ x -> T $ \ y -> x
s = T $ \ f -> T $ \ g -> T $ \ x -> (f ! x) ! (g ! x)
Это прекрасно работает и позволяет создавать и выполнять произвольные лямбда-выражения. Например, мы можем легко создать функцию, которая превращает Int в число Чёрча:
zero = k ! i
succ = s ! (s ! (k ! s) ! k)
encode 0 = zero
encode n = succ ! (encode $ n-1)
Опять же, это работает отлично.
Теперь напишите функцию декодирования.
Да, удачи с этим! Проблема в том, что мы можем создавать произвольные лямбда-термы, но мы не можем их инспектировать каким-либо образом. Поэтому нам нужно добавить какой-то способ сделать это.
На данный момент лучшая идея, которую я придумал, заключается в следующем:
data Term x = F (Term x -> Term x) | R (Term x -> x)
F f ! x = f x
R f ! x = R $ \ _ -> f x
out :: Term x -> x
out (R f) = f (error "mu")
out (F _) = (error "nu")
i = F $ \ x -> x
k = F $ \ x -> F $ \ y -> x
s = F $ \ f -> F $ \ g -> F $ \ x -> (f ! x) ! (g ! x)
Теперь я могу сделать что-то вроде
decode :: Term Int -> Int
decode ti = out $ ti ! R (\ tx -> 1 + out tx) ! R (\ tx -> 0)
Это отлично работает для церковных булов и церковных цифр.
Дела начинают идти ужасно неправильно, когда я начинаю пытаться делать что-то высокоуровневое. Отбросив всю информацию о типах для реализации нетипизированного лямбда-исчисления, я теперь изо всех сил пытаюсь убедить средство проверки типов позволить мне делать то, что я хочу.
Это работает:
something = F $ \ x -> F $ \ n -> F $ \ s -> s ! x
nothing = F $ \ n -> F $ \ s -> n
encode :: Maybe x -> Term x
encode (Nothing) = nothing
encode (Just x) = something ! x
Это не:
decode :: Term x -> Maybe (Term x)
decode tmx = out $ tmx ! R (\ tx -> Nothing) ! R (\ tx -> Just tx)
Я пробовал дюжину небольших вариаций этого; ни один из них не проверяет тип. Дело не в том, что я не понимаю, почему это терпит неудачу, а в том, что я не могу придумать, как добиться успеха. (В частности, R Just явно плохо набрано.)
Как будто мне нужна функция forall x y. Term x -> Term y. Потому что для чистых нетипизированных терминов это всегда должно быть возможно. Это не сработает только в терминах, связанных с R. Но я не могу понять, как сформулировать это в системе типов Haskell.
(Например, попробуйте изменить тип F на forall x. Term x -> Term x. Теперь определение k имеет неправильный тип, поскольку внутреннее F $ \ y -> x не может фактически возвращать любой тип, а только [теперь исправлено] тип x .)
У кого-нибудь умнее меня есть идея получше?
