GADTs，TypeFamilies類型推理在實現「mixins」時失敗

Question

我想用可組合邏輯創建複雜的數據結構。也就是說，數據結構具有通用格式（實質上是一些記錄，其中某些字段的類型可以更改）以及一些通用函數。具體結構具有通用功能的具體實現。

我嘗試了兩種方法。一種是使用類型系統（具有類型類型，類型族，函數依賴關係等）。另一個是創建我自己的「vtable」並使用GADT。兩種方法都以類似的方式失敗 - 似乎有一些基本的東西我在這裏失蹤。或者，也許有更好的Haskell方法來做到這一點？

這裏是失敗 「輸入」 代碼：

{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE FunctionalDependencies #-} 
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TemplateHaskell #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeSynonymInstances #-} 

module Typed where 

import Control.Monad.State 
import Data.Lens.Lazy 
import Data.Lens.Template 

-- Generic Block. 
data Block state ports = Block { _blockState :: state, _blockPorts :: ports } 

-- For the logic we want to use, we need some state and ports. 
data LogicState = LogicState { _field :: Bool } 
data LogicPorts incoming outgoing = 
    LogicPorts { _input :: incoming, _output :: outgoing } 

makeLenses [ ''Block, ''LogicState, ''LogicPorts ] 

-- We need to describe how to reach the needed state and ports, 
-- and provide a piece of the logic. 
class LogicBlock block incoming outgoing | block -> incoming, block -> outgoing where 
    logicState :: block ~ Block state ports => Lens state LogicState 
    logicPorts :: block ~ Block state ports => Lens ports (LogicPorts incoming outgoing) 
    convert :: block ~ Block state ports => incoming -> State block outgoing 
    runLogic :: State block outgoing 
    runLogic = do 
    state <- access $ blockState 
    let myField = state ^. logicState ^. field 
    if myField 
    then do 
     ports <- access blockPorts 
     let inputMessage = ports ^. logicPorts ^. input 
     convert inputMessage 
    else 
     error "Sorry" 

-- My block uses the generic logic, and also maintains additional state 
-- and ports. 
data MyState = MyState { _myLogicState :: LogicState, _myMoreState :: Bool } 
data MyPorts = MyPorts { _myLogicPorts :: LogicPorts Int Bool, _myMorePorts :: Int } 

makeLenses [ ''MyState, ''MyPorts ] 

type MyBlock = Block MyState MyPorts 

instance LogicBlock MyBlock Int Bool where 
    logicState = myLogicState 
    logicPorts = myLogicPorts 
    convert x = return $ x > 0 

-- All this work to write: 
testMyBlock :: State MyBlock Bool 
testMyBlock = runLogic 

這將導致以下錯誤：

Typed.hs:39:7: 
    Could not deduce (block ~ Block state1 ports1) 
    from the context (LogicBlock block incoming outgoing) 
     bound by the class declaration for `LogicBlock' 
     at Typed.hs:(27,1)-(41,19) 
     `block' is a rigid type variable bound by 
       the class declaration for `LogicBlock' at Typed.hs:26:18 
    Expected type: StateT block Data.Functor.Identity.Identity outgoing 
     Actual type: State (Block state1 ports1) outgoing 
    In the return type of a call of `convert' 
    In a stmt of a 'do' block: convert inputMessage 

這裏是失敗的 「虛函數表」 代碼：

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE RecordWildCards #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TemplateHaskell #-} 

module VTable where 

import Control.Monad.State 
import Data.Lens.Lazy 
import Data.Lens.Template 

-- Generic Block. 
data Block state ports = Block { _blockState :: state, _blockPorts :: ports } 

-- For the logic we want to use, we need some state and ports. 
data LogicState = LogicState { _field :: Bool } 
data LogicPorts incoming outgoing = 
    LogicPorts { _input :: incoming, _output :: outgoing } 

makeLenses [ ''Block, ''LogicState, ''LogicPorts ] 

-- We need to describe how to reach the needed state and ports, 
-- and provide a piece of the logic. 
data BlockLogic block incoming outgoing where 
    BlockLogic :: { logicState :: Lens state LogicState 
       , logicPorts :: Lens ports (LogicPorts incoming outgoing) 
       , convert :: incoming -> State block outgoing 
       } 
      -> BlockLogic (Block state ports) incoming outgoing 

-- | The generic piece of logic. 
runLogic :: forall block state ports incoming outgoing 
      . block ~ Block state ports 
     => BlockLogic block incoming outgoing 
     -> State block outgoing 
runLogic BlockLogic { .. } = do 
    state <- access $ blockState 
    let myField = state ^. logicState ^. field 
    if myField 
    then do 
    ports <- access blockPorts 
    let inputMessage = ports ^. logicPorts ^. input 
    convert inputMessage 
    else 
    error "Sorry" 

-- My block uses the generic logic, and also maintains additional state and ports. 
data MyState = MyState { _myLogicState :: LogicState, _myMoreState :: Bool } 
data MyPorts = MyPorts { _myLogicPorts :: LogicPorts Int Bool, _myMorePorts :: Int } 

makeLenses [ ''MyState, ''MyPorts ] 

type MyBlock = Block MyState MyPorts 

-- All this work to write: 
testMyBlock :: State MyBlock Bool 
testMyBlock = runLogic $ BlockLogic 
         { logicState = myLogicState 
         , logicPorts = myLogicPorts 
         , convert = \x -> return $ x > 0 
         } 

它導致出現以下錯誤：

VTable.hs:44:5: 
    Could not deduce (block1 ~ Block state1 ports1) 
    from the context (block ~ Block state ports) 
     bound by the type signature for 
       runLogic :: block ~ Block state ports => 
          BlockLogic block incoming outgoing -> State block outgoing 
     at VTable.hs:(37,1)-(46,17) 
    or from (block ~ Block state1 ports1) 
     bound by a pattern with constructor 
       BlockLogic :: forall incoming outgoing state ports block. 
           Lens state LogicState 
           -> Lens ports (LogicPorts incoming outgoing) 
           -> (incoming -> State block outgoing) 
           -> BlockLogic (Block state ports) incoming outgoing, 
       in an equation for `runLogic' 
     at VTable.hs:37:10-26 
     `block1' is a rigid type variable bound by 
       a pattern with constructor 
       BlockLogic :: forall incoming outgoing state ports block. 
           Lens state LogicState 
           -> Lens ports (LogicPorts incoming outgoing) 
           -> (incoming -> State block outgoing) 
           -> BlockLogic (Block state ports) incoming outgoing, 
       in an equation for `runLogic' 
       at VTable.hs:37:10 
    Expected type: block1 
     Actual type: block 
    Expected type: StateT 
        block1 Data.Functor.Identity.Identity outgoing 
     Actual type: State block outgoing 
    In the return type of a call of `convert' 
    In a stmt of a 'do' block: convert inputMessage 

我不明白爲什麼當整個事情明確地在ScopedTypeVariables和「forall block」下時，GHC正在執行「block1」。

編輯＃1：增加了功能依賴關係，這要感謝Chris Kuklewicz指出了這一點。但問題依然存在。

編輯＃2：正如克里斯指出的那樣，在VTable解決方案中，擺脫所有「塊〜塊狀態端口」而不是寫入「塊狀態端口」解決了這個問題。

編輯＃3：好的，所以問題似乎是，對於每個單獨的函數，GHC都需要參數中足夠的類型信息來推導出所有類型的所有類型，即使對於根本不使用的類型。因此，在上述（例如）logicState的情況下，參數僅給我們提供狀態，這不足以知道端口和傳入和傳出類型是什麼。不要緊，它對logicState函數無關緊要; GHC想知道，也不能，所以編譯失敗。如果這確實是核心原因，那麼GHC在編譯邏輯狀態刪除時直接抱怨會更好 - 它似乎有足夠的信息來檢測那裏的問題;如果我在那個地方看到一個問題說「端口類型沒有被使用/確定」，它會更清晰。編輯＃4：我還不清楚爲什麼（塊〜塊狀態端口）不起作用;我想我用它來達到一個無意的目的？它似乎應該有效。我同意克里斯使用CPP來解決這個問題是一種令人憎惡的行爲。但寫「B t r p e」（在我的真實代碼中有更多的參與者）也不是一個好的解決方案。

Answer 1

我有一個行修復您的VTable代碼：

  , convert :: incoming -> State block outgoing 

成爲

  , convert :: incoming -> State (Block state ports) outgoing 

那麼你應該簡化runLogic類型

runLogic :: BlockLogic (Block state ports) incoming outgoing 
     -> State (Block state ports) outgoing 

PS：更多細節回答下面的評論。

消除「阻止〜」不是修復的一部分。通常「〜」只在instance a~b => ... where的情況下需要。

以前如果我給一個函數a xxx :: BlockLogic (Block state ports) incoming outgoing那麼它可以解壓convert xxx :: State block outgoing。但新的block與(Block state ports)完全不相關，它是一種新的不可知的類型。編譯器在名稱的末尾附加一個數字以使block1出現在錯誤消息中。

原始代碼（兩個版本）都存在編譯器可以從給定上下文中推斷出哪些類型的問題。

至於詳細程度，請嘗試type。不要使用CPP和DEFINE。

type B s p = BlockLogic (Block s p) 

runLogic :: B s p i o -> State (Block s p) o 

PPS：進一步解釋類版本的問題。如果我代替（塊SP）塊，並添加你所提到的函數依賴：

class LogicBlock state ports incoming outgoing | state ports -> incoming outgoing where 
    logicState :: Lens state LogicState 
    logicPorts :: Lens ports (LogicPorts incoming outgoing) 
    convert :: incoming -> State (Block state ports) outgoing 

使用logicState指甲下來state但留下ports不明，使得ports#

使用logicPorts指甲下來ports但留下state不明，使ports#

編譯runLogic運行到端口，端口0，端口1和狀態，狀態0，狀態1之間的許多類型不匹配錯誤。

這些操作似乎並不適合放在相同的類型類中。你可以把它們分成不同的類型類，或者在類聲明中加入「，state-> ports，ports-> state」函數依賴關係。