haskell - 专门化未使用的类型变量时不可触及的类型

Question

我正在为我的 haskell 程序创建一个 eDSL，它允许定义一组指令来存储数据。这些指令可能会相互依赖结果，甚至序列化到文件中以进一步恢复。这是我想出的一些东西(相当冗长，但这是我可以提取来重现我的问题的最少代码量):

{-# LANGUAGE TypeFamilies, RankNTypes, ExistentialQuantification, FlexibleContexts #-}
module Untouchable where

import Control.Applicative
import Control.Monad.Writer
import System.Random

class ResultClass e where
  type ResultMonad :: * -> *
  statementAResult :: ResultMonad (e Int)
  literalResult    :: a -> ResultMonad (e a)

data Statement result = StatementA | StatementB (result Int)
data StatementWithResult result t = StatementWithResult (Statement result, result t)
data AnyStatementWithResult result = forall t. AnyStatementWithResult (StatementWithResult result     t)
type Program result a = (ResultClass result, ResultMonad ~ m) => WriterT [AnyStatementWithResult     result] m a

doA :: Program result (result Int)
doA = do
  r <- lift statementAResult
  tell [AnyStatementWithResult $ StatementWithResult (StatementA, r)]
  return r

doB :: result Int -> Program result ()
doB arg = do
  r <- lift $ literalResult ()
  tell [AnyStatementWithResult $ StatementWithResult (StatementB arg, r)]

prog :: Program result ()
prog = do
  x <- doA
  doB x

data PrettyPrintResult x = PrettyPrintResult Int
  deriving Show

instance ResultClass PrettyPrintResult where
  type ResultMonad = IO
  statementAResult = PrettyPrintResult <$> randomIO
  literalResult _ = PrettyPrintResult <$> randomIO

printProg :: Program PrettyPrintResult a -> IO ()
printProg p = do
  stmts <- execWriterT p
  forM_ stmts $ \(AnyStatementWithResult (StatementWithResult (stmt, r))) -> do
    putStrLn $ "Statement: " ++ case stmt of
      StatementA -> "A"
      StatementB arg -> "B with arg " ++ show arg
    putStrLn $ "Result: " ++ show r

test :: IO ()
test = printProg prog

问题本身在于 printProg 函数，该函数预计会漂亮地打印 eDSL block 。我希望它能够适用于所有程序，无论其返回类型如何。但 GHC 提示道:

untouchable.hs: line 52, column 18:
  Couldn't match type `a0' with `()'
    `a0' is untouchable
      inside the constraints (ResultClass PrettyPrintResult,
                              ResultMonad ~ m)
      bound by a type expected by the context:
                 (ResultClass PrettyPrintResult, ResultMonad ~ m) =>
                 WriterT [AnyStatementWithResult PrettyPrintResult] m a0
      at untouchable.hs:52:8-21
  Expected type: WriterT
                   [AnyStatementWithResult PrettyPrintResult] m a0
    Actual type: WriterT
                   [AnyStatementWithResult PrettyPrintResult] m ()
  In the first argument of `printProg', namely `prog'
  In the expression: printProg prog

如果我用 Program PrettyPrintResult () -> IO () 替换 printProg 的签名，一切都会构建，甚至按预期工作。

所以问题是为什么 GHC 无法匹配类型变量，而该类型变量实际上被代码忽略了？我如何重写 printProg(或者代码的其他部分)以使其接受所有程序，无论其结果类型如何？

Answer 1

这与Program 类型同义词的约束有关。将 printProg 的类型签名替换为 real 类型:

printProg :: WriterT [AnyStatementWithResult PrettyPrintResult] IO a -> IO () 

它将编译。必须确定约束m ~ ResultMonad(给定的m是给定结果的ResultMonad吗？)，但 m 是存在的，并且没有其他信息可以帮助决定这一点。为什么错误说 a 不可触及，我不知道。如果您想要良好的类型错误，请不要在类型同义词中添加约束!以下更改也解决了您的问题:

type Program result a = 
  (ResultClass result) => WriterT [AnyStatementWithResult result] ResultMonad a

最后，这些问题是一个更大问题的症状。请注意以下事项:

*Untouchable> :t lift statementAResult
lift statementAResult
  :: (ResultClass e, MonadTrans t) => t IO (e Int)

ResultMonad 立即变成 IO!这当然是错误的。发生这种情况的原因是 lift 有一个 Monad 约束，并且无法获取 Monad ResultMonad - 因为 ResultMonad > 取决于 result 类型，但 ResultMonad 中任何地方都没有 result。本质上，您的 result 和 ResultMonad 类型已变得完全无关。

简单的解决方法是使用函数依赖而不是类型族:

class Monad m => ResultClass e m | e -> m where
  statementAResult :: m (e Int)
  literalResult    :: a -> m (e a)

您不需要 Monad m 约束，但大概您的结果 monad 必须始终是 monad。然后，简单地编写您的 Program 类型，没有任何限制:

type Program result m a = WriterT [AnyStatementWithResult result] m a

并将所有约束放入它们出现的函数类型中:

doA :: ResultClass result m => Program result m (result Int)

doB :: ResultClass result m => result Int -> Program result m ()

prog :: ResultClass result m => Program result m ()

-- etc ...

现在使用 lift 不再“忘记”您的结果 monad 类型:

*Untouchable> :t lift statementAResult
lift statementAResult
  :: (ResultClass e m, MonadTrans t) => t m (e Int)