idris - 错误 monad 的 VerifiedMonad 实例

Question

我正在尝试为以下数据类型完成 monadLeftIdentity 证明:

data ErrorM : (a : Type) -> Type where
  AllGood : a -> ErrorM a
  Error : String -> ErrorM a

instance Monad ErrorM where
  (AllGood x) >>= f = f x
  (Error err) >>= f = Error err

instance VerifiedMonad ErrorM where
  monadApplicative (AllGood f) (AllGood x) = Refl
  monadApplicative (Error err) (AllGood x) = Refl
  monadApplicative (AllGood f) (Error err) = Refl
  monadApplicative (Error er1) (Error er2) = Refl
  monadLeftIdentity x f = ?z

我省略了 Functor、Applicative 及其对应的 Verified 的实例，因为它们非常冗长和琐碎。请告诉我，可以将它们全部粘贴到这里。

我已经尝试将 return x 重写为 pure x 或 AllGood x，但没有成功(重写确实与证明状态无关)。

我也试过像这样优化 return x:

  monadLeftIdentity x f with (return x)
    monadLeftIdentity x' f | AllGood x' = ?z

但我收到以下错误信息:

 `-- Error.idr line 51 col 22:
     When elaborating left hand side of with block in Prelude.Monad.Astra.Error.ErrorM instance of Prelude.Monad.VerifiedMonad, method monadLeftIdentity:
     Can't match on with block in Prelude.Monad.Astra.Error.ErrorM instance of Prelude.Monad.VerifiedMonad, method monadLeftIdentity a (AllGood x') x' b f return

如何解决这个问题？

Answer 1

这似乎是 Idris 类型检查器中的一个错误，即使它们完全由类型决定，它也不会解析重载函数。

为了证明，我可以这样证明:

myLeftIdentity : (x : a) -> (f : a -> ErrorM b) -> return x >>= f = f x
myLeftIdentity x f = Refl

它的类型检查很好，但它不能用作实例中的见证:

instance VerifiedMonad ErrorM where
  monadApplicative (AllGood _) (AllGood _) = Refl
  monadApplicative (Error _) _ = Refl
  monadApplicative (AllGood _) (Error _) = Refl

  monadLeftIdentity = myLeftIdentity

结果

 Can't unify
         (x : a) -> (f : a -> ErrorM b) -> return x >>= f = f x
 with
         (x : a) -> (f : a -> ErrorM b) -> Main.ErrorM instance of Prelude.Monad.Monad, method >>= (return x) f = f x

即使两个 >>= 应该是一样的。

有趣的是，我能够通过定义我自己版本的 Monad 和 VerifiedMonad 类来解决这个问题:

infixl 5 >>=>

class Applicative m => Monad' (m : Type -> Type) where
  (>>=>) : m a -> (a -> m b) -> m b

return' : Monad' m => a -> m a
return' = pure

instance Monad' ErrorM where
  (AllGood x) >>=> f = f x
  (Error err) >>=> f = Error err

class (Monad' m, VerifiedApplicative m) => VerifiedMonad' (m : Type -> Type) where
  monadLeftIdentity : (x : a) -> (f : a -> m b) -> return' x >>=> f = f x

instance VerifiedMonad' ErrorM where
  monadLeftIdentity x f = Refl