待办事项GADTs打破等式推理哈斯克尔

我使用ProgramT从业务包待办事项GADTs打破等式推理哈斯克尔

{-# LANGUAGE GADTs #-} 
import Control.Monad ((<=<)) 
import Control.Monad.Operational 

data Motor' a where 
    --Define GADT 

serialNewportT :: (Monad m, MonadIO m) => ProgramT Motor' m a -> m a 
serialNewportT = eval <=< viewT 
    where 
    eval :: (Monad m, MonadIO m) => ProgramViewT Motor' m v -> m v 
    eval (Return x) = return x 
    eval (x :>>= k) = f x >>= serialNewportT . k 

f :: (Monad m, MonadIO m) => Motor' a -> m a 
f = undefined -- excluded for brevity

代码如下解释，因为它的立场，目前类型检查就好了。但是，我希望能够切换解释器如何处理不同的电机，所以我想使f成为一个参数，而不是硬编码。我尝试使用以下代码进行此开关：

{-# LANGUAGE GADTs #-} 
import Control.Monad ((<=<)) 
import Control.Monad.Operational 

data Motor' a where 
    --Define GADT 

serialNewportT :: (Monad m, MonadIO m) => (Motor' a -> m a) -> ProgramT Motor' m a -> m a 
serialNewportT f = eval <=< viewT 
    where 
    eval :: (Monad m, MonadIO m) => ProgramViewT Motor' m v -> m v 
    eval (Return x) = return x 
    eval (x :>>= k) = f x >>= serialNewportT f . k

但是，此代码失败，出现错误消息

Couldn't match type ‘b’ with ‘c’ 
    ‘b’ is a rigid type variable bound by 
     a pattern with constructor 
     :>>= :: forall (instr :: * -> *) (m :: * -> *) a b. 
       instr b -> (b -> ProgramT instr m a) -> ProgramViewT instr m a, 
     in an equation for ‘eval’ 
    ‘c’ is a rigid type variable bound by 
     the type signature for 
     serialNewportT :: (Monad m, MonadIO m) => 
          (Motor' c -> m c) -> ProgramT Motor' m a -> m a 
Expected type: Motor' c 
    Actual type: Motor' b

因为我只是与同类型的局部更换一个全球的名字，我还以为它应该顺利工作过。我怎样才能得到类型与f作为一个参数统一？

来源

2016-04-25 user640078

您没有正确翻译F'的'类型。在原始代码中，它可以通过类型'Motor'a'对任何'a'实例化，但是在非工作代码中，您声明它的类型与'ProgramT Motor'中的'a'完全相同。，而在函数体中，你可以在'Motor'b'上调用'f'来寻找其他的（存在量化的）类型'b'。您可能只需要更高的排名类型：'serialNewportT ::（Monad m，MonadIO m）=>（全部x。Motor'x - > mx） - > ProgramT Motor'ma - > ma' – user2407038

@ user2407038似乎是一个答案给我 – Carsten

呃。我对范围类型变量进行了大量研究，试图让所有内容匹配，但没有考虑N级类型。我想现在该是最后学习的时候了。 @ user2407038，如果你想让这个答案，我会给你信贷。 – user640078

您尚未正确翻译f的类型。在原始代码中，f的类型是forall a . (..) => Motor' a -> m a。它可以用一个类型Motor' a实例化任何a，但在非工作代码，你的国家，它的类型是完全相同的a在ProgramT Motor' m a，而在函数体，你在Motor' b其他一些（称之为f存在量化）类型b。

你只需要一个更高级别类型：

serialNewportT :: (Monad m, MonadIO m) => (forall x . Motor' x -> m x) -> ProgramT Motor' m a -> m a

来源

2016-04-26 13:38:00 user2407038

待办事项GADTs打破等式推理哈斯克尔

回答

相关问题