类型只匹配haskell中的函数 [英] Type matches only inside a function in haskell

问题描述

我是哈斯克尔的初学者，并试图实施自然数的教会编码，正如本指南< a>。

  { - ＃LANGUAGE RankNTypes＃ - } 
 
 newtype Chur = Chr（forall a （a  - > a） - >（a  - > a））
 
 zero :: Chur 
 zero = Chr（\xy  - > y）
 
  - 教会到int 
 c2i :: Chur  - >整数
 c2i（Chr cn）= cn（+ 1）0 
 
  - 这个工程
 i1 = c2i零
  - 这不是
 i2 =零（+ 1）0 
  

对于 i2


 无法匹配预期的类型'（Integer  - > Integer） - >整数 - > t'
与实际类型'Chur'
相关的绑定包括i2 :: t（绑定在test.hs：14：1）
函数'zero'应用于两个参数
但其类型'Chur'没有
在表达式中：零（+ 1）0 
在'i2'的等式中：i2 =零（+ 1）0 
  

如果包装在函数中， Chur 可以带参数，但不能没有它？

解决方案

Chur 包装在函数中的参数 - 包装在 Chur 中的函数确实：

  c2i（Chr cn）= cn（+ 1）0 
  

cn 是包含在 Chur 中的函数。

您可以使用替换方法看看会发生什么：

  c2i zero 
 ==> c2i（Chr（\ xy  - > y））
 ==>> （\ x y  - > y）（+ 1）0 
 ==> 0 
  

但是

 零（+ 1）0 
 ==> （Chr（\xy-> y））（+ 1）0 
  

因为（Chr（\xy - > y））不是一个函数。

d written

  c2i :: Chur  - >整数
 c2i cn = cn（+ 1）0 
  

您会看到类似的错误。

I'm a beginner in haskell, and trying to implement the Church encoding for natural numbers, as explained in this guide.

{-# LANGUAGE RankNTypes #-}

newtype Chur = Chr (forall a. (a -> a) -> (a -> a))

zero :: Chur
zero = Chr (\x y -> y)

-- church to int
c2i :: Chur -> Integer
c2i (Chr cn) = cn (+ 1) 0

-- this works
i1 = c2i zero
-- this doesn't
i2 = zero (+ 1) 0

For i2 I get a type mismatch:

Couldn't match expected type ‘(Integer -> Integer) -> Integer -> t’
            with actual type ‘Chur’
Relevant bindings include i2 :: t (bound at test.hs:14:1)
The function ‘zero’ is applied to two arguments,
but its type ‘Chur’ has none
In the expression: zero (+ 1) 0
In an equation for ‘i2’: i2 = zero (+ 1) 0

How come Chur can take arguments when wrapped in a function, but can't without it?

解决方案

Chur doesn't take any arguments when wrapped in the function - the function wrapped in Chur does:

c2i (Chr cn) = cn (+ 1) 0

Here, cn is the function wrapped inside a Chur.

You can use the substitution method to see what's happening:

    c2i zero
==> c2i (Chr (\x y -> y))
==> (\x y -> y) (+ 1) 0
==> 0

But

    zero (+ 1) 0
==> (Chr (\x y -> y)) (+ 1) 0

which doesn't work since (Chr (\x y -> y)) is not a function.

If you'd written

c2i :: Chur -> Integer
c2i cn = cn (+ 1) 0

you would have seen a similar error.

这篇关于类型只匹配haskell中的函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！