haskell - 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

这是失败的“vtable”代码:

{-# 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

我不明白为什么 GHC 会选择“block1”，因为整个事情都明确地在 ScopedTypeVariables 和“forall block”之下。

编辑 #1:添加了功能依赖项，感谢 Chris Kuklewicz 指出这一点。问题仍然存在。

编辑 #2:正如 Chris 指出的那样，在 VTable 解决方案中，摆脱所有“块 ~ 块状态端口”，而是到处写“块状态端口”可以解决问题。

编辑 #3:好的，所以问题似乎是对于每个单独的函数，GHC 需要参数中有足够的类型信息来推断所有类型，即使是根本不使用的类型。所以在(例如)上面的 logicState 的情况下，参数只给我们状态，这不足以知道端口和传入和传出类型是什么。没关系，这对 logicState 函数并不重要； GHC 想知道，但不能，所以编译失败。如果这确实是核心原因，那么GHC在编译 logicState decleration 时直接提示会更好——它似乎有足够的信息来检测那里的问题；如果我在那个位置看到一个问题，说“未使用/确定端口类型”，它会更清楚。

编辑 #4:我仍然不清楚为什么 (block ~ Block state ports) 不起作用；我想我将它用于意外目的？看起来它应该有效。我同意 Chris 的观点，即使用 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:更详细地回答下面的评论。

消除“block ~”不是修复的一部分。通常只有在 instance a~b => ... where 中才需要“~”情况。

以前如果我给一个函数一个 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:进一步解释类版本问题。如果我将 (Block s p) 替换为 block 并添加您提到的功能依赖项:

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