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”函数依赖关系。