Экземпляр VerifiedMonad для монады ошибки

Я пытаюсь завершить доказательство 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

Как это сделать?


idris
person Chetan    schedule 12.02.2015    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Это похоже на ошибку в программе проверки типов 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
person Cactus    schedule 12.02.2015
comment
Я зарегистрировал его как github.com/idris-lang/Idris-dev/ Issues/1913 с разработчиками Idris - person Cactus; 12.02.2015