阴阳拼图哈斯克尔版:种类不兼容错误 [英] Haskell version of yin-yang puzzle : Kind incompatibility error

查看:124
本文介绍了阴阳拼图哈斯克尔版:种类不兼容错误的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

我要实现的阴阳难题在Haskell。这是我的尝试(unsucceful):

   - 使用的数据类型是递归的,所以我们必须定义一个newtype b $ b newtype Cl m = Cl {goOn :: MonadCont m => Cl m  - > m(Cl m)} 

yinyang ::(MonadIO m,MonadCont m)=> m(Cl m)
yinyang = do
yin< - (callCC $ \\ k - > return(Cl k))>> =(\c - > liftIO(putStr (callC $ \\ k→> return(Cl k))>> =(\c->< liftIO(putStr> *)>> goOn c)
goOn yin yang

类型,显然 callCC $ \k - >返回(Cl k)给出 m(Cl m),所以 yin 是键入 Cl m yang 是同样的事情。所以我期望 goOn yin yang 给出最终的类型 m(Cl m)



这个实现看起来不错,但问题是它不能编译!这是我得到的错误:

 无法将种类'*'与`*  - > *'
匹配类型时的种类不兼容性:
m0 :: * - > *
Cl ::(* - > *) - > *
在'goOn'的第一个参数中,也就是'yin'
在'do'区块中:go yin yang

有什么想法可以解决这个问题吗?

更新



虽然我自己找到答案,但我仍然不明白错误消息的含义。任何人都可以向我解释?我所知道的是,在问题版本中, goOn c 返回类似于 Cl m - > m(Cl m),而不是预期的 m(Cl m)。但这不是你能从错误信息中得到的。

解决方案

代码中存在一个愚蠢的错误。这里是正确的实现方式

  newtype CFix m = CFix {goOn :: CFix m  - > m(CFix m)} 

yinyang ::(MonadIO m,MonadCont m)=> m(CFix m)
yinyang = do
yin< - (\c-> liftIO(putStr@)>> return c)=<< (callCC $ \ k - > return(CFix k))
yang< - (\ c - > liftIO(putStr*)>> return c)=< (callCC $ \k-> return(CFix k))
goOn yin yang

这很容易运行。

  main :: IO()
main = runContT yinyang $ void。返回

甚至

  main :: IO()
main = runContT yinyang undefined

虽然后者看起来很可怕,但它是安全的,因为延续永远不会有机会进行评估。 (整体表达式将被评估为值 _ | _ ,因为它永远不会停止)



结果

  @ * @ ** @ *** ... 

解释

最初的尝试是直接翻译Scheme版本

 (let *(
(yin
((lambda(cc)(display#\ @) cc)(call-with-current-continuation(lambda(c)c))))
(yang
((lambda(cc)(display#\ *)cc) (b)(b)(b)(b)(b)到Haskell。对于类型化语言来说,进行上述类型检查的关键是要有一个类型为 t 的类型,该类型与 t - >吨。在Haskell中,这是通过使用 newtype 关键字完成的。另外,为了产生副作用,我们需要 IO ,但它不支持 callCC 。为了支持以后,我们需要 MonadCont 。因此,为了处理这两者,我们需要 MonadIO MonadCont 。此外, newtype 必须知道它正在处理哪个 Monad ,所以它应该携带 Monad 作为其类型参数。所以现在我们写:

  newtype CFix m = ... 

yinyang ::(MonadIO m, MonadCont m)=> m(CFix m)

由于我们在 Monad 使用 do 表示法很方便。因此 let * 赋值应该被翻译为 yin < - 并且 yang < - 。在 MonadIO display 中,我们使用 liftIO.putStr call-with-current-continuation 转换为 callCC ,但显然我们不能转换为 id 之类的。让我们稍等片刻。

我的错误是天真地翻译显示块的组合运算符和 callCC 阻止到>> = 。在Scheme或其他严格的语言中,参数要在表达式之前进行评估,因此 callCC 块应在显示块之前执行。因此,我们将使用 = << 来代替>> = 。该代码现在看起来像

  newtype CFix m = ... 

yinyang ::(MonadIO m ,MonadCont m)=> m(CFix m)
yinyang = do
yin< - (\c-> liftIO(putStr@)>> return c)=<< (callCC $ ...)
yang< - (\ c - > liftIO(putStr*)>> return c)=< (callCC $ ...)
...

现在是时候制作了键入check并查看我们应该在 ... 中放置什么。 callCC 的签名是

  MonadCont m => ((a  - > m b) - > m a) - > ma 

所以它的参数有类型

  MonadCont m => (a  - > m b) - > ma 

对于某些类型 a b 。通过查看迄今为止编写的代码,我们很容易得出结论: yin yang 应该具有相同类型的 callCC s返回值 ma 。但是,原始模式版本使用 yin yang 作为函数,因此它们的类型为 p - > [R 。所以这里是我们需要递归类型和 newtype



获取 ma 直接的方法是使用 return ,我们需要一些类型为 a 的东西。假设这是来自我们要定义的类型构造函数。现在为 callCC 提供参数,我们需要从(a - >>)构造一个 a mb)个。所以这就是构造函数的样子。但是什么是 b ?一个简单的选择是使用相同的 a 。所以我们定义 CFix

  newtype CFix m = CFix {goOn :: CFix m  - > m(CFix m)} 

以及 callCC 的参数

  \k  - > (CFIX k)

我们使用 CFix 构造函数从给定的参数构造 CFix ,并使用 return 将其包装为所需的类型。



现在,我们如何使用 yin (类型为 m(CFix m))作为一个函数?类型析构函数 goOn 允许我们提取内部函数,所以我们定义了最后一个 ...

  newtype CFix m = CFix {goOn :: CFix m  - > m(CFix m)} 

yinyang ::(MonadIO m,MonadCont m)=> m(CFix m)
yinyang = do
yin< - (\c-> liftIO(putStr@)>> return c)=<< (callCC $ \ k - > return(CFix k))
yang< - (\ c - > liftIO(putStr*)>> return c)=< (callCC $ \k-> return(CFix k))
goOn yin yang

这是该程序的最终版本。


I want to implement the yin-yang puzzle in Haskell. Here is my attempt (unsucceful):

-- The data type in use is recursive, so we must have a newtype defined
newtype Cl m = Cl { goOn :: MonadCont m => Cl m -> m (Cl m) }

yinyang :: (MonadIO m, MonadCont m) => m (Cl m)
yinyang = do
    yin <-  (callCC $ \k -> return (Cl k)) >>= (\c -> liftIO (putStr "@") >> goOn c)
    yang <- (callCC $ \k -> return (Cl k)) >>= (\c -> liftIO (putStr "*") >> goOn c)
    goOn yin yang

When look at the types, obviously callCC $ \k -> return (Cl k) gives a m (Cl m), so yin is of type Cl m. yang is the same thing. So I expect goOn yin yang gives the final type m (Cl m).

This implementation looks good, but the problem is it does not compile! here is the error I got:

Couldn't match kind `*' against `* -> *'
Kind incompatibility when matching types:
  m0 :: * -> *
  Cl :: (* -> *) -> *
In the first argument of `goOn', namely `yin'
In a stmt of a 'do' block: goOn yin yang

Any idea to fix this?

UPDATE

Although I found the answer by myself, I still don't understand what that error message means. Can any one explain to me? What I know already is, in the problematic version, goOn c returns something like Cl m -> m (Cl m), not the expected m (Cl m). But that is not what you can get from the error message.

解决方案

There is a stupid error in the code. Here is the correct implementation

newtype CFix m = CFix { goOn :: CFix m -> m (CFix m) }

yinyang :: (MonadIO m, MonadCont m) => m (CFix m)
yinyang = do
    yin <-  (\c -> liftIO (putStr "@") >> return c) =<< (callCC $ \k -> return (CFix k)) 
    yang <- (\c -> liftIO (putStr "*") >> return c) =<< (callCC $ \k -> return (CFix k)) 
    goOn yin yang

It is very easy to run this.

main :: IO ()
main = runContT yinyang $ void.return

or even

main :: IO ()
main = runContT yinyang undefined

Although the later looks scary, but it is safe because the continuation will never have the chance to be evaluated. (The overall expression, will be evaluated to value _|_ because it never stops)

It outputs the expected result

@*@**@***...

Explained

The original attempt is to directly translate the Scheme version

(let* (
 (yin
    ((lambda (cc) (display #\@) cc) (call-with-current-continuation (lambda (c) c))))
 (yang
    ((lambda (cc) (display #\*) cc) (call-with-current-continuation (lambda (c) c)))))
(yin yang))

into Haskell. For a typed language, the key to make the above type check is to have a type t that isomorphic to t -> t. In Haskell this is done by using newtype keyword. Also, to have side effects we need IO, but it does not support callCC. To support the later we need MonadCont. So to work with both we need MonadIO and MonadCont. Also, the newtype must know which Monad it is working on, so it shall carry the Monad as its type parameter. So now we write

newtype CFix m = ...

yinyang :: (MonadIO m, MonadCont m) => m (CFix m)

Since we are wroking on a Monad it is convenient to use do notation. So let* assignments shall be translated to yin <- and yang <-. In a MonadIO to display we use liftIO.putStr. The call-with-current-continuation translate to callCC but obviously we cannot translate to id or the like. Let's leave this for a moment.

My mistake is naively translate the combination operator of the display block and the callCC block to >>=. In Scheme or other strict language, the parameter is to be evaluated before the expression, so the callCC block shall execute before the display block. As a result, we shall use =<< instead of >>=. The code is now looks

newtype CFix m = ...

yinyang :: (MonadIO m, MonadCont m) => m (CFix m)
yinyang = do
    yin <- (\c -> liftIO (putStr "@") >> return c) =<< (callCC $ ...)
    yang <- (\c -> liftIO (putStr "*") >> return c) =<< (callCC $ ...)
    ...

Now it is time to make it type check and see what shall we put in the ...s. callCCs signature is

MonadCont m => ((a -> m b) -> m a) -> m a

so its parameter have type

MonadCont m => (a -> m b) -> m a

for some type a and b. By looking at the code written so far, we easily conclude that yin and yang shall have the same type of callCCs return value m a. However, the original schema version uses yin and yang as functions so they have type p -> r. So here is where we need recursive types and newtype.

To obtain a m a the straight forward method is use return, and we need something have type a. Let's suppose this is came from the type constructor that we are going to define. Now to supply parameter for callCC we need to construct an a from (a -> m b). So this is what the constructor would looks like. But what is b? An easy choice is to use the same a. so we have the definition of CFix:

newtype CFix m = CFix { goOn :: CFix m -> m (CFix m) }

and an implementation of the callCC's parameter

\k -> return (CFix k)

we use CFix constructor to construct a CFix from the given parameter, and use return to wrap it to the desired type.

Now, how do we use yin (of type m (CFix m)) as a function? The type destructor goOn allow us to extract the inner function, so we have the definition for the last ....

newtype CFix m = CFix { goOn :: CFix m -> m (CFix m) }

yinyang :: (MonadIO m, MonadCont m) => m (CFix m)
yinyang = do
    yin <-  (\c -> liftIO (putStr "@") >> return c) =<< (callCC $ \k -> return (CFix k)) 
    yang <- (\c -> liftIO (putStr "*") >> return c) =<< (callCC $ \k -> return (CFix k)) 
    goOn yin yang

This is final version of the program.

这篇关于阴阳拼图哈斯克尔版:种类不兼容错误的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆