Haskell:函数签名

Question

该程序编译没有问题:

bar :: MonadIO m
    => m String
bar = undefined

run2IO :: MonadIO m
       => m String
       -> m String
run2IO foo  = liftIO bar

当我bar改为foo(参数名称)时,

run2IO :: MonadIO m
       => m String
       -> m String
run2IO foo  = liftIO foo

我明白了:

无法将类型'm'与'IO'匹配'm'是一个刚性类型变量,由run2IO :: MonadIO的类型签名绑定m => m String - > m String ...

预期类型:IO String实际类型:m String ...

为什么这两个案例不相同？

Answer 1

记住以下类型liftIO:

liftIO :: MonadIO m => IO a -> m a

重要的是,第一个参数必须是具体的IO值.这意味着当你有一个表达式liftIO x,那么x必须是类型IO a.

当Haskell函数被普遍量化(使用隐式或显式forall)时,这意味着函数调用者选择替换类型变量的内容.作为一个例子,考虑id函数:它有类型a -> a,但是当你评估表达式时id True,则id获取类型Bool -> Bool因为a实例化为Bool类型.

现在,再考虑一下你的第一个例子:

run2IO :: MonadIO m => m Integer -> m Integer
run2IO foo = liftIO bar

这个foo论点在这里完全无关紧要,所以真正重要的是liftIO bar表达式.由于liftIO 要求其第一个参数是类型IO a,因此bar 必须是类型IO a.然而,bar是多态的:它实际上有类型MonadIO m => m Integer.

幸运的是,IO有一个MonadIO实例,所以使用to 实例化该bar值,这是可以的,因为它是普遍量化的,所以它的实例化是通过它的使用来选择的.IOIO Integerbar

现在,考虑另liftIO foo一种使用的情况.这似乎是一样的,但它实际上根本不存在:这次,MonadIO m => m Integer值是函数的参数,而不是单独的值.量化是在整个函数上,而不是单个值.要更直观地理解这一点,id再次考虑可能会有所帮助,但这一次,请考虑其定义:

id :: a -> a
id x = x

在这种情况下,x无法实例化为Bool在其定义范围内,因为这意味着id只能处理Bool值,这显然是错误的.实际上,在实现中id,x必须完全使用 - 它不能被实例化为特定类型,因为这会违反参数保证.

因此,在您的run2IO函数中,foo必须完全一般地用作任意MonadIO值,而不是特定MonadIO实例.该liftIO调用尝试使用IO不允许的特定实例,因为调用者可能不提供IO值.

当然,您可能希望以与原样相同的方式量化函数的参数bar; 也就是说,您可能希望实例选择其实例化,而不是调用者.在这种情况下,您可以使用RankNTypes语言扩展名使用显式指定其他类型forall:

{-# LANGUAGE RankNTypes #-}

run3IO :: MonadIO m => (forall m1. MonadIO m1 => m1 Integer) -> m Integer
run3IO foo = liftIO foo

这将是类型检查,但它不是一个非常有用的功能.

Answer 2

在第一个,你使用liftIO上bar.这实际上需要bar :: IO String.现在,IO碰巧是(通常)一个实例MonadIO,所以这是有效的 - 编译器只是抛弃了多态性bar.

在第二种情况下,编译器无法决定使用哪种特定monad作为其类型foo:它由环境修复,即调用者可以决定MonadIO它应该是什么实例.要再次获得选择IOmonad 的自由,您需要以下签名:

{-# LANGUAGE Rank2Types, UnicodeSyntax #-}

run2IO' :: MonadIO m
       => (? m' . MonadIO m' => m' String)
       -> m String
run2IO' foo  = liftIO foo

......但是我不认为你真的想要那样:你也可以写下来

run2IO' :: MonadIO m => IO String -> m String
run2IO' foo  = liftIO foo

或者干脆run2IO = liftIO.