Можно представить практически любой тип, который вы хотите. Но поскольку монадические операции выполняются по-разному для каждого типа, это не можно написать >>= один раз и заставить его работать для каждого экземпляра.
Однако, вы можете написать общие функции, которые зависят от доказательств из экземпляра класса типов. Рассмотрим 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: они работают точно так же, как и другие «общие» методы Monad, которые мы определили: сначала им нужно дать доказательства Monad-ness, а затем они функционируют должным образом.
Мы можем представлять Maybe как функцию, которая принимает 2 входа, первая - это функция для выполнения, если она равна Just x, а вторая - это значение, чтобы заменить ее, если она не указана.
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
Так как лямбда-исчисления Тьюринга можно кодировать любой вычислительный процесс в нем. Я предполагаю, что речь идет именно о кодировании. Конечно, нетипизированное исчисление не имеет в нем типов, но можно кодировать некоторые объекты, которые ведут себя как типы и механизмы ввода. Точно так же, как у него нет bools и numbers, но есть соответствующие кодировки, указанные в вопросе. [Answer by Dan] (https://stackoverflow.com/a/8936209/707926) в большей степени соответствует этому пониманию. –