haskell - 「ミックスイン」を実装する際の GADT、TypeFamilies の型推論の失敗

Question

構成可能なロジックを使用して複雑なデータ構造を作成しようとしています。つまり、データ構造には、一般的な形式 (基本的には、型が変更される可能性のあるいくつかのフィールドを持つレコード) といくつかの一般的な関数があります。特定の構造には、汎用関数の特定の実装があります。

私が試した2つのアプローチがあります。1 つは、型システムを使用することです (型クラス、型ファミリ、関数依存などを使用)。もう 1 つは、独自の「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

全体が明示的に ScopedTypeVariables と "forall block" の下にあるのに、GHC が "block1" を選択する理由がわかりません。

編集 #1: これを指摘してくれた Chris Kuklewicz のおかげで、機能的な依存関係が追加されました。ただし、問題は残ります。

編集＃2：クリスが指摘したように、VTableソリューションでは、すべての「ブロック〜ブロック状態ポート」を取り除き、代わりに「ブロック状態ポート」をどこにでも書くことで問題が解決します。

編集＃3：OK、問題は、GHCがすべてのタイプを推測するために、すべての個別の関数に対して、パラメーターに十分なタイプ情報を必要とすることです。まったく使用されていないタイプであっても。したがって、上記の (たとえば) logicState の場合、パラメーターは状態のみを提供し、ポートと着信および発信の型が何であるかを知るには十分ではありません。logicState 関数にとって実際には問題にならないことは気にしないでください。GHC は知りたがっていますが、知ることができないため、コンパイルは失敗します。これが本当に核心的な理由なら、logicState 宣言をコンパイルするときに GHC が直接文句を言う方がよかったでしょう - そこに問題を検出するのに十分な情報があるようです。その場所で「ポートタイプが使用されていない/決定されていない」という問題を見ていたら、もっと明確だったでしょう。

編集＃4：（ブロック〜ブロック状態ポート）が機能しない理由はまだわかりません。意図しない目的で使用していると思いますか？うまくいくはずだったようです。CPP を使用して回避することは忌まわしいことであるという Chris の意見に同意します。しかし、「B trp e」(より多くのパラメーターを持つ私の実際のコード) を書くことも良い解決策ではありません。

score 4 · Accepted Answer

VTableコードを1行修正しました。

            , 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状況でのみ必要です。

以前は、関数にaxxx :: 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 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すると、ports、ports0、ports1とstate、state0、state1の間で多くのタイプの不一致エラーが発生します。

これらの操作は、同じ型クラスに一緒に収まらないようです。それらを別々の型クラスに分割するか、クラス宣言に「、状態->ポート、ポート->状態」の機能依存性を追加することができます。

haskell - 「ミックスイン」を実装する際の GADT、TypeFamilies の型推論の失敗

1 に答える 1

Related

Reference