3

我正在尝试完成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，因为它们非常冗长和琐碎。让我知道，可以把它们都贴在这里。ApplicativeVerified

我试图重写return x为pure xor 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

怎么办？

4

1 回答 1

4

这似乎是 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

即使两者>>=应该是一回事。

有趣的是，我可以通过定义自己的MonadandVerifiedMonad类版本来解决这个问题：

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
于 2015-02-12T10:39:25.287 回答