待辦事項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打破等式推理哈斯克爾

回答

相關問題