VerifiedFunctor - доказать карту (карта g) x = x - PullRequest
Новая
       96

VerifiedFunctor - доказать карту (карта g) x = x

0 голосов
/ 24 августа 2018

Я пытаюсь доказать утверждение об интерфейсе VerifiedFunctor (метод Functor, который map учитывает идентичность и состав): 

interface Functor f => VerifiedFunctor (f : Type -> Type) where
    functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) ->
                      (x : f a) -> map g x = x

Вот утверждение (которое логически говорит, что map . map для двух заданных функторов также учитывает идентичность): 

functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
                         (g : a -> a) -> ((v : a) -> g v = v) ->
                         (x : f2 (f1 a)) -> map (map g) x = x
functorIdentityCompose fnId prId = functorIdentity (map fnId) (functorIdentity fnId prId)

Однако я получаю следующую ошибку: 

Type mismatch between
        (x : f1 a) -> map fnId x = x (Type of functorIdentity fnId prId)
and
        (v : f a) -> map fnId v = v (Expected type)

Specifically:
        Type mismatch between
                f1 a
        and
                f a

Я попытался указать все неявные аргументы: 

functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
                         {a : Type} -> {f1 : Type -> Type} -> {f2 : Type -> Type} ->
                         (g : a -> a) -> ((v : a) -> g v = v) -> (x : f2 (f1 a)) ->
                         map {f=f2} {a=f1 a} {b=f1 a} (map {f=f1} {a=a} {b=a} g) x = x

... Но получил еще одну ошибку: 

When checking argument func to function Prelude.Functor.map:
        Can't find implementation for Functor f15

Так есть идеи, что здесь не так и как доказать это утверждение?

1 Ответ

0 голосов
/ 24 августа 2018

Вот эвристика: когда «очевидные» вещи не работают ... эта-расширяйся!Так что это работает: 

functorIdentityCompose : (VerifiedFunctor f1, VerifiedFunctor f2) =>
  (g : a -> a) -> ((v : a) -> g v = v) ->
  (x : f2 (f1 a)) -> map (map g) x = x
functorIdentityCompose fnId prId x =
  functorIdentity (map fnId) (\y => functorIdentity fnId prId y) x

Похоже, что полное приложение запускает поиск экземпляров.

...