时间戳

首页 > 解决方案 > 看似无可辩驳的 GADT 模式上的失败匹配

haskell - 看似无可辩驳的 GADT 模式上的失败匹配

问题描述

继续我反对MonadFail成为我的 monad 约束的运动，我现在面临以下问题：

data Thing :: Bool -> Type where
  TrueThing :: Thing 'True
  FalseThing :: Thing 'False

myFunc :: Monad m => m ()
myFunc = do
  TrueThing <- return TrueThing
  return ()

哪个不会编译，因为您猜对了：

• Could not deduce (MonadFail m)
    arising from a do statement
    with the failable pattern ‘TrueThing’

事实上，如果我阅读了我能找到的关于该主题的任何1 个文档，那么匹配应该如何在 GADT 上工作还不是很清楚。我显然会认为这个案子属于“无条件匹配”的范畴。但我承认它不符合“单一构造函数data类型”<sup>2 的条件。尽管避免这种歧义是首先使用 GADT 的重点。

当然~lazyPattern有效，但这只是创可贴。我已经对比赛进行了脱糖：

myFunc' :: Monad m => m ()
myFunc' = let f :: _
              f TrueThing = return ()
          in return TrueThing >>= f

现在，虽然错误消息不是那么明确 ( Couldn't match expected type ‘p’ with actual type ‘m0 ())，但类型通配符更能说明问题：

• Found type wildcard ‘_’ standing for ‘Thing a -> p’

…并引导我找到“解决方案”：

myFunc' :: forall m. Monad m => m ()
myFunc' = let f :: Thing 'True -> m ()
              f TrueThing = return ()
          in return TrueThing >>= f

嗯，这行得通。我可以把它加糖吗？ f不会出现在初始表达式中，但是我可以用类型注释两个点：一元表达式和模式。我分别尝试过，也尝试过一起尝试，都是“无法推断MonadFail”。

我想我的期望太高了，但我想知道为什么。它是某种类型推断限制吗？一个GADT？我一开始就没有使用正确的机器吗？这种模式怎么会失败呢？

(1) 在这个问题上很难找到权威。GHC 手册提到 MonadFail，但链接到HaskellPrime wiki，这似乎是Haskell wiki上同一页面的旧版本

Bool(2) 也以()作品代替。但就我的实际问题而言，这太过简单了。

标签： haskellmonadsgadt

解决方案

这可能不会是一个完全令人满意的答案，但无论如何我想分享我的发现。

我从一个确实可能出现模式匹配失败的情况开始，修改您的 GADT 以添加另一个构造函数'True。然后我添加了一个MonadFail上下文，只是为了让 ti 编译，然后看看它在哪里使用。

{-# LANGUAGE GADTs , DataKinds, KindSignatures #-}
{-# OPTIONS -Wall #-}

import Data.Kind
import Control.Monad.Fail

data Thing :: Bool -> Type where
  TrueThing :: Thing 'True
  FalseThing :: Thing 'False
  TrueThing2 :: Thing 'True

myFunc :: (Monad m, MonadFail m) => m ()
myFunc = do
  TrueThing <- return TrueThing
  return ()

上面的代码产生以下核心：

myFunc
  = \ (@ (m_a1mR :: * -> *))
      _ [Occ=Dead]
      ($dMonadFail_a1mU :: MonadFail m_a1mR) ->
      let {
        $dMonad1_a1nj :: Monad m_a1mR
        [LclId]
        $dMonad1_a1nj
          = Control.Monad.Fail.$p1MonadFail @ m_a1mR $dMonadFail_a1mU } in
      >>=
        @ m_a1mR
        $dMonad1_a1nj
        @ (Thing 'True)
        @ ()
        (return
           @ m_a1mR $dMonad1_a1nj @ (Thing 'True) GADTmonad.$WTrueThing)
        (\ (ds_d1ol :: Thing 'True) ->
           case ds_d1ol of {
             TrueThing co_a1n5 ->
               return @ m_a1mR $dMonad1_a1nj @ () GHC.Tuple.();
             TrueThing2 ipv_s1ph ->
               Control.Monad.Fail.fail
                 @ m_a1mR
                 $dMonadFail_a1mU
                 @ ()
                 (GHC.CString.unpackCString#
                    "Pattern match failure in do expression at GADTmonad.hs:15:3-11"#)
           })

上面，我们可以看到：

  • Monad正在传递的字典myFunc被丢弃！相反，字典是从字典中恢复的MonadFail（包括字典Monad）。我不知道为什么 GHC 更喜欢那个。
  • MonadFail字典用于处理最后一场比赛中的情况TrueThing2。这是意料之中的。

现在，如果我们删除TrueThing2构造函数，我们会得到以下核心：

myFunc
  = \ (@ (m_a1mJ :: * -> *))
      _ [Occ=Dead]
      ($dMonadFail_a1mM :: MonadFail m_a1mJ) ->
      let {
        $dMonad1_a1nb :: Monad m_a1mJ
        [LclId]
        $dMonad1_a1nb
          = Control.Monad.Fail.$p1MonadFail @ m_a1mJ $dMonadFail_a1mM } in
      >>=
        @ m_a1mJ
        $dMonad1_a1nb
        @ (Thing 'True)
        @ ()
        (return
           @ m_a1mJ $dMonad1_a1nb @ (Thing 'True) GADTmonad.$WTrueThing)
        (\ (ds_d1od :: Thing 'True) ->
           case ds_d1od of { TrueThing co_a1mX ->
           return @ m_a1mJ $dMonad1_a1nb @ () GHC.Tuple.()
           })

现在TrueThing2情况消失了，并且fail从MonadFail.

但是，出于某种原因，Monad仍然可以通过字典获取MonadFail字典，即使现在可以避免这种情况。

我的猜测是这是当前 GHC 的限制。原则上它可以脱糖，生成核心，然后观察到MonadFail不需要的。但是，我认为类型检查是在这些步骤发生之前执行的，此时 GHC 为最坏的情况做准备，MonadFail以后可能仍然需要。我不知道应该添加多少工作以使其在类型检查期间更智能并避免需要MonadFail，除非确实需要。

推荐阅读