Иногда мы спрашиваем людей о внедрении нетипизированного лямбда-исчисления в Haskell. [Естественно, я теперь не могу найти ни одного из этих вопросов, но я уверен, что видел их!] Просто для хихиканья, я думал, что я немного поиграю с этим.
Это достаточно тривиально, чтобы сделать что-то вроде
i = \ x -> x
k = \ x y -> x
s = \ f g x -> (f x) (g x)
Это прекрасно работает. Однако, как только вы попытаетесь сделать что-то вроде
s i i
проверяющий тип правильно жалуется на бесконечный тип. В основном все в нетипизированном лямбда-исчислении является функцией — что по существу означает, что все функции имеют бесконечную arity. Но Хаскелл допускает только функции конечной арности. (Потому что, действительно, зачем вам бесконечная арность?)
Ну, оказывается, мы можем легко обойти это ограничение:
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)
Опять же, это работает отлично.
Теперь напишите функцию декодирования.
& hellip; да, удачи в этом! Беда в том, что мы можем создать произвольные лямбда-термины, но мы не можем их каким-либо образом проверить. Поэтому нам нужно добавить какой-то способ сделать это.
Пока, лучшая идея, которую я придумал, заключается в следующем:
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.)
У кого-нибудь умнее меня есть лучшая идея?
