当我学习教会编码并尝试降低复杂性时,我使用elm
来实现代码。但我找到了一个我无法弄清楚类型签名的观点。
type alias Peano = (Int -> Int) -> Int -> Int
fwd : Int -> Int
fwd x = x + 1
c3 : Peano
c3 f =
f >> f >> f
cExp: ???
cExp cm cn =
cn cm
但是,在elm-repl
> cExp cm cn = cn cm
<function> : a -> (a -> b) -> b
> cExp c3
<function> : (((a -> a) -> a -> a) -> b) -> b
> cExp c3 c3
<function> : (a -> a) -> a -> a
> cExp c3 c3 fwd
<function> : number -> number
> cExp c3 c3 fwd 0
27 : number
因此,在功能思维中使用等式推理,我将类型替换为:
a -> (a -> b) -> b
as
Peano -> (Peano -> (Int -> Int)) -> (Int -> Int)
^ ^
fwd 0
因此,
cExp c3 c3 fwd 0 = 27
可能是什么问题呢?
我想知道这是一个与elm
中的无限类型相关的问题,但我没有足够的知识来理解正在发生的事情。
问题是你用Peano
来定义Int
,当真正的参数可能是函数时。你应该让它更通用:
type alias Peano a = (a -> a) -> a -> a
现在你必须更新你的教会数字:
c3 : Peano a
c3 f =
f >> f >> f
(旁注:Elm的>>
算子是函数组合,但反方向。使用常规函数组合运算符<<
可能更惯用,这相当于Haskell的.
运算符)
你的指数函数可以这样注释:
cExp : a -> (a -> b) -> b
cExp cm cn =
cn cm