Встраивание типов с более высоким родом (монады!) В нетипизированное лямбда-исчисление - PullRequest
7 голосов
/ 19 января 2012

Можно кодировать различные типы в нетипизированном лямбда-исчислении с помощью функций более высокого порядка.

Examples:
zero  = λfx.      x
one   = λfx.     fx
two   = λfx.   f(fx)
three = λfx. f(f(fx))
etc

true  = λtf. t
false = λtf. f

tuple = λxyb. b x y
null  = λp. p (λxy. false)

Мне было интересно, проводилось ли какое-либо исследование по внедрению других менее традиционных типов.Было бы замечательно, если бы была какая-то теорема, которая утверждает, что любой тип может быть внедрен.Возможно, существуют ограничения, например, могут быть встроены только типы *.

Если действительно возможно представить менее традиционные типы, было бы здорово увидеть пример.Мне особенно интересно узнать, как выглядят члены класса монад.

Ответы [ 3 ]

17 голосов
/ 20 января 2012

Можно представить практически любой тип, который вы хотите. Но поскольку монадические операции реализуются по-разному для каждого типа, не можно написать >>= один раз и заставить его работать для каждого экземпляра.

Однако вы можете написать универсальные функции, которые зависят от свидетельства экземпляра класса типов. Рассмотрим e здесь как кортеж, где fst e содержит определение «связывания», а snd e содержит определение «возврата».

bind = λe. fst e    -- after applying evidence, bind looks like λmf. ___
return = λe. snd e  -- after applying evidence, return looks like λx. ___

fst = λt. t true
snd = λt. t false

-- join x = x >>= id
join = λex. bind e x (λz. z)

-- liftM f m1 = do { x1 <- m1; return (f x1) }
-- m1 >>= \x1 -> return (f x1)
liftM = λefm. bind e m (λx. return e (f x))

Затем вам нужно будет определить «кортеж доказательств» для каждого экземпляра Монады. Обратите внимание, что способ, которым мы определили bind и return: они работают так же, как и другие «общие» методы монады, которые мы определили: им сначала нужно дать свидетельство монадности, а затем они функционируют как и ожидалось.

Мы можем представить Maybe как функцию, которая принимает 2 входа, первая - это функция, которую нужно выполнить, если она равна Just x, а вторая - значение, которое нужно заменить, если оно равно Nothing.

just = λxfz. f x
nothing = λfz. z

-- bind and return for maybes
bindMaybe = λmf. m f nothing
returnMaybe = just

maybeMonadEvidence = tuple bindMaybe returnMaybe

Списки похожи, представляют Список как его функцию свертывания. Следовательно, список - это функция, которая принимает 2 входа: «против» и «пустой». Затем он выполняет foldr myCons myEmpty в списке.

nil = λcz. z
cons = λhtcz. c h (t c z)

bindList = λmf. concat (map f m)
returnList = λx. cons x nil

listMonadEvidence = tuple bindList returnList

-- concat = foldr (++) []
concat = λl. l append nil

-- append xs ys = foldr (:) ys xs
append = λxy. x cons y

-- map f = foldr ((:) . f) []
map = λfl. l (λx. cons (f x)) nil

Either тоже просто. Представляет любой тип как функцию, которая принимает две функции: одну для применения, если это Left, и другую для применения, если это Right.

left = λlfg. f l
right = λrfg. g r

-- Left l >>= f = Left l
-- Right r >>= f = f r
bindEither = λmf. m left f
returnEither = right

eitherMonadEvidence = tuple bindEither returnEither

Не забывайте, функции сами по себе (a ->) образуют монаду. И все в лямбда-исчислении является функцией ... так что ... не думай об этом слишком усердно. ;) Вдохновлен непосредственно из источника Control.Monad.Instances

-- f >>= k = \ r -> k (f r) r
bindFunc = λfkr. k (f r) r
-- return = const
returnFunc = λxy. x

funcMonadEvidence = tuple bindFunc returnFunc
12 голосов
/ 19 января 2012

Вы смешиваете уровень типа с уровнем значения. В нетипизированном лямбда-исчислении нет монад. Могут быть монадические операции (уровень значения), но не монады (уровень типа). Однако сами операции могут быть одинаковыми, поэтому вы не потеряете выразительную силу. Так что сам вопрос на самом деле не имеет смысла.

1 голос
/ 19 января 2012

Ну, у нас уже есть кортежи и логические значения, поэтому мы можем представить Either и, в свою очередь, любой нерекурсивный тип суммы, основанный на этом:

type Either a b = (Bool, (a, b))
type Maybe a    = Either () a

И, возможно, является членом класса типа Monad. Перевод лямбда-нотации оставлен в качестве упражнения.

...