haskell Church编码的数字列表的和/积不进行类型检查

b4lqfgs4 于 2023-10-19 发布在其他

关注(0)|答案(2)|浏览(127)

按照Church编码的自然数和右折叠表示的列表的标准定义，我想写一个函数，它以一个数字列表作为参数，并返回其元素的总和：

type Number = forall a. (a -> a) -> a -> a

type List a = forall b. (a -> b -> b) -> b -> b

zero :: Number
zero _ x = x

plus :: Number -> Number -> Number
plus a b f x = a f (b f x)

sum :: List Number -> Number
sum xs = xs plus zero

sum的定义没有类型检查-我假设这是因为它的类型扩展为

(forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a)

而函数定义要求

forall a. ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a

实际上，它会进行类型检查：

sum :: List ((a -> a) -> a -> a) -> (a -> a) -> a -> a  -- OK
sum xs = xs plus' zero
  where
    plus' :: (t1 -> t -> t3) -> (t1 -> t2 -> t) -> t1 -> t2 -> t3  -- inferred by compiler
    plus' a b f x = a f (b f x)
    zero _ x = x

我能以某种方式避免在所有定义中复制(a -> a) -> a -> a吗？结果类型变得非常长非常快...我能做

type Number a = (a -> a) -> a -> a

并将其放在类型注解中，但也许我可以做一些更聪明/更巧妙的事情？

haskell

来源：https://stackoverflow.com/questions/76857889/sum-product-of-church-encoded-list-of-numbers-does-not-type-check

2条答案

按热度按时间

eblbsuwk1#

在具有快速查看不可预测性的GHC版本（9.2及更新版本）中，您可以通过启用ImpredicativeTypes扩展来使原始的sum函数工作。

赞(0）回复(0）举报 2023-10-19

mrzz3bfm2#

您可以在newtype中隔离类型。这似乎起作用：

{-# LANGUAGE RankNTypes #-}

newtype Number = Number {num :: forall a. (a -> a) -> a -> a}

newtype List a = List {lst :: forall b. (a -> b -> b) -> b -> b}

plus :: Number -> Number -> Number
plus a b = Number (\f x -> (num a) f ((num b) f x))

zero :: Number
zero = Number (\_ x -> x)

sum :: List Number -> Number
sum xs = (lst xs) plus zero

赞(0）回复(0）举报 2023-10-19

我来回答

haskell Church编码的数字列表的和/积不进行类型检查

2条答案

相关问题

热门标签

最新问答