标签: church-encoding

我必须实现haskell map函数来处理教会列表,其定义如下:

type Churchlist t u = (t->u->u)->u->u

在lambda演算中,列表编码如下:

[] := ?c. ?n. n
[1,2,3] := ?c. ?n. c 1 (c 2 (c 3 n))

本练习的示例解决方案是:

mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u)
mapChurch f l = \c n -> l (c.f) n

我不知道这个解决方案是如何工作的,我不知道如何创建这样的功能.我已经体验过lambda演算和教堂数字,但是这个练习对我来说是一个很大的问题,我必须能够在下周的考试中理解并解决这些问题.有人可以给我一个很好的消息来源,我可以学习如何解决这些问题,或者给我一些关于它是如何工作的指导？

我试图在Haskell中实现教堂数字,但我遇到了一个小问题.Haskell抱怨无限类型

发生检查:无法构造无限类型:t =(t - > t1) - >(t1 - > t2) - > t2

当我尝试做减法时.我99%肯定我的lambda演算是有效的(虽然如果不是,请告诉我).我想知道的是,我能做些什么来让haskell与我的功能一起工作.

module Church where

type (Church a) = ((a -> a) -> (a -> a))

makeChurch :: Int -> (Church a)
makeChurch 0 = \f -> \x -> x
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x)

numChurch x = (x succ) 0

showChurch x = show $ numChurch x

succChurch = \n -> \f -> \x -> f (n f x) …

我正在通过SICP工作,问题2.6让我陷入了困境.在处理教会数字时,将零和1编码为满足某些公理的任意函数的概念似乎是有意义的.另外,使用零的定义导出单个数字的直接公式,并且add-1函数是有意义的.我不明白如何形成一个加号运算符.

到目前为止,我有这个.

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

通过wikipedia条目查看lambda演算,我发现plus的定义是PLUS:=λmnfx.mf(nfx).使用该定义,我能够制定以下程序.

(define (plus n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

我不明白的是,如何仅使用先前派生的程序给出的信息直接导出该过程.任何人都可以用某种严格的证明形式回答这个问题吗？直觉上,我想我明白发生了什么,但正如Richard Feynman曾经说过的那样,"如果我不能建造它,我就无法理解......"

我正在玩Haskell中的一些lambda演算,特别是教堂数字.我有以下定义:

let zero = (\f z -> z)
let one = (\f z -> f z)
let two = (\f z -> f (f z))
let iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))
let mult = (\m n -> (\s z -> m (\x -> n s x) z))

这有效:

:t (\n -> (iszero n) one (mult one one))

发生检查时失败:

:t (\n -> (iszero n) one (mult n one))

我iszero和 …

或者具体来说,为什么我们使用foldr来编码列表和迭代来编码数字？

对于长篇介绍很抱歉,但我真的不知道如何命名我想问的事情,所以我需要先给一些说明.这很大程度上吸引了这个CAMcCann的帖子,这个帖子只是不太满足我的好奇心,而且我也会用Rank-n-types和无限懒惰的东西来处理这些问题.

将数据类型编码为函数的一种方法是创建"模式匹配"函数,该函数为每种情况接收一个参数,每个参数是一个函数,它接收与该构造函数对应的值以及返回相同结果类型的所有参数.

对于非递归类型,这一切都符合预期

--encoding data Bool = true | False
type Bool r = r -> r -> r

true :: Bool r
true = \ct cf -> ct

false :: Bool r
false = \ct cf -> cf

--encoding data Either a b = Left a | Right b
type Either a b r = (a -> r) -> (b -> r) -> r

left :: a -> Either a b r
left x …

教会编码(又名访客模式)是一种将数据表示为函数的方式:而不是

data T = C1 F1 F2 | C2 F3 F4

你可以定义

data T = T (forall r. (F1 -> F2 -> r) -> (F3 -> F4 -> r) -> r)

.虽然将任何东西表示为函数的能力很好,但我一直认为第一个版本更可取,因为它更清晰,并且不需要语言扩展(显式forall).但是,您有时可以在公共图书馆中找到教会编码的数据.使用它有什么好处？

公共图书馆中教会编码的例子:

• Iteratee
• 修订控制monad
• (请帮我扩展名单)

记住这个计划:

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (sum)

type List h = forall t . (h -> t -> t) -> t -> t

sum_ :: (Num a) => List a -> a
sum_ = \ list -> list (+) 0

toList :: [a] -> List a
toList = \ list cons nil -> foldr cons nil list

sum :: (Num a) => [a] -> a
-- sum = sum_ . toList        -- does not work
sum = \ …

我正在通过软件基础工作,目前正在进行关于教会数字的练习.这是自然数的类型签名:

Definition nat := forall X : Type, (X -> X) -> X -> X.

我已经定义了一个succ类型的函数nat -> nat.我现在想定义一个这样的加法函数:

Definition plus (n m : nat) : nat := n nat succ m.

但是,我收到以下错误消息:

Error: Universe inconsistency.

这个错误信息实际意味着什么？

我一直在努力研究如何在Scala中实现Church编码的数据类型.它似乎需要rank-n类型,因为你需要一个类型的第一类const函数forAll a. a -> (forAll b. b -> b).

但是,我能够如此编码对:

import scalaz._

trait Compose[F[_],G[_]] { type Apply = F[G[A]] }

trait Closure[F[_],G[_]] { def apply[B](f: F[B]): G[B] }

def pair[A,B](a: A, b: B) =
  new Closure[Compose[({type f[x] = A => x})#f,
                      ({type f[x] = B => x})#f]#Apply, Id] {
    def apply[C](f: A => B => C) = f(a)(b)
  }

对于列表,我能够编码cons:

def cons[A](x: A) = {
  type T[B] = B => (A => B => …

这是一个有文化的haskell帖子.只需将其保存为"ChurchList.lhs"即可运行它.

> {-# LANGUAGE Rank2Types #-}

教会编码列表是一种通过函数表示列表的方式.它类似折叠和延续传递风格.

> newtype ChurchList a = CList {runCList :: forall r. (a -> r -> r) -> r -> r}

为了说明这对应于列表,这里是O(n)同构

> fromList :: [a] -> ChurchList a
> fromList xs = CList $ \cons empty -> foldr cons empty xs

> toList :: ChurchList a -> [a]
> toList cl = runCList cl (:) []

> instance Show a => Show (ChurchList a) where
>   show cl = "fromList " ++ show (toList …