标签: scott-encoding

或者具体来说,为什么我们使用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 …

这是一个有文化的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 …

当我声明这个新类型时:

newtype ListScott a = 
  ListScott { 
  unconsScott :: (a -> ListScott a -> r) -> r -> r 
}

这将定义假设的rank-2类型ListScott :: ((a -> ListScott a -> r) -> r -> r) -> ListScott a,编译器抱怨r不在范围内.从类型签名中可以看出我想要传递一个第一类多态函数ListScott吗？

为什么我需要这样的r情况下的显式类型量词？

我不是一个类型理论家,可能忽略了一些东西......

我一直在使用Free的数据类型Control.Monad.Free从free包.现在我想将其转换为使用F中Control.Monad.Free.Church,但无法弄清楚如何将功能映射.

例如,使用的简单模式匹配函数Free看起来像这样 -

-- Pattern match Free
matchFree
  :: (a -> r)
  -> (f (Free f a) -> r)
  -> Free f a
  -> r
matchFree kp _ (Pure a) = kp a
matchFree _ kf (Free f) = kf f

我可以轻松地将其F转换为通过转换为/从Free- 使用的函数

-- Pattern match F (using toF and fromF)
matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) …

Scott 编码列表可以定义如下：

newtype List a =
    List {
      uncons :: forall r. r -> (a -> List a -> r) -> r
    }

与 ADT 版本相反的List是类型和数据构造函数。Scott 编码通过模式匹配来确定 ADT，这实质上意味着删除一层构造函数。这是uncons没有隐式参数的完整操作：

uncons :: r -> (a -> List a -> r) -> List a -> r
--    Nil ^    ^^^^^^^^^^^^^^^^^^ Cons
uncons nil cons (List f) = f nil cons

这是完全有道理的。uncons接受一个常数、一个延续和 aList并产生任何值。

然而，数据构造函数的类型对我来说没有多大意义：

List :: (forall r. r -> (a -> List a -> r) …

假设我有一个scott编码的列表,例如:

scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n))))

我想要一个接收这种类型的列表并将其转换为实际列表([1,2,3])的函数,除了这样的函数不能递归.也就是说,它必须是eta-beta正常形式.这个功能存在吗？