Ошибка «перезапись не изменила тип» для визуально одинаковых типов - PullRequest
Новая
       90

Ошибка «перезапись не изменила тип» для визуально одинаковых типов

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

Я написал короткую функцию: 

swapMaybe : Monad m => Maybe (m a) -> m (Maybe a)
swapMaybe Nothing = pure Nothing
swapMaybe (Just x) = map Just x

Тогда я попытался доказать одно из его свойств: 

import Interfaces.Verified

swapMaybePreservesMap : VerifiedMonad m => (g : a -> b) -> (x : Maybe (m a)) ->
                        swapMaybe (map (map g) x) = map (map g) (swapMaybe x)
swapMaybePreservesMap g Nothing = ?hswapMaybePreservesMapNothing
swapMaybePreservesMap g (Just x) = ?hswapMaybePreservesMapJust
    (functorComposition x g Just)
    (functorComposition x Just (map g))

:t hswapMaybePreservesMapJust дает следующий тип: 

  a : Type
  b : Type
  g : a -> b
  m : Type -> Type
  x : m a
  constraint : VerifiedMonad m
--------------------------------------
hswapMaybePreservesMapJust : (map (\x1 => Just (g x1)) x = map Just (map g x)) ->
                             (map (\x1 => Just (g x1)) x = map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)) ->
                             map Just (map g x) = map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)

Визуально одна и та же левая сторона map (\x1 => Just (g x1)) x обоих параметров hswapMaybePreservesMapJust выглядит многообещающе для применения rewrite.

Однако, это терпит неудачу: 

swapMaybePreservesMap g (Just x) = rewrite (functorComposition x g Just) in 
    (functorComposition x Just (map g))

Ошибка: 

When checking right hand side of swapMaybePreservesMap with expected type
        swapMaybe (map (map g) (Just x)) = map (map g) (swapMaybe (Just x))

rewriting map (\x1 => Just (g x1)) x to map Just (map g x) did not change type map Just (map g x) =
                                                                               map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)

Я проверил этот вопрос и попытался явно указать тип результата с помощью the, переместив параметры rewrite в let и eta-expand map g. Также безуспешно, хотя: 

swapEq : {x : a} -> {y : a} -> x = y -> y = x
swapEq eq = rewrite eq in Refl

swapMaybePreservesMap : VerifiedMonad n => (g : a -> b) -> (x : Maybe (n a)) ->
                        swapMaybe (map (\z => map g z) x) = map (\z => map g z) (swapMaybe x)
swapMaybePreservesMap g Nothing = ?hswapMaybePreservesMapNothing
swapMaybePreservesMap g xx@(Just x) = let
    pr1 = (swapEq $ functorComposition x g Just)
    pr2 = (functorComposition x Just (\z => map g z))
    in the (swapMaybe (map (\z => map g z) xx) = map (\z => map g z) (swapMaybe xx))
        (rewrite pr1 in pr2)

... со следующим сообщением: 

When checking right hand side of swapMaybePreservesMap with expected type
        swapMaybe (map (\z => map g z) (Just x)) = map (\z8 => map g z8) (swapMaybe (Just x))

When checking argument value to function Prelude.Basics.the:
        rewriting map Just (map g x) to map (\x1 => Just (g x1)) x did not change type map Just (map g x) =
                                                                                       map (\z11 => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g z11) (map Just x)

Как я прочитал в документах : 

rewrite prf in expr

Если у нас есть prf : x = y, а для expr требуется тип Для свойства x синтаксис rewrite ... in будет искать x в требуемый тип expr и замените его на y.

Почему rewrite не работает в этом случае?

Это из-за действительно разных значений в левой части параметров (может быть, некоторые неявные параметры не показаны) или что-то еще? Может, лучше применить какой-нибудь скрипт тактики Elab явно?

1 Ответ

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

Наконец-то я нашел причину - это ограничения разных типов в swapMaybe и swapMaybePreservesMap. Следующая реализация дает явную ошибку: 

swapMaybePreservesMap : VerifiedMonad m => (g : a -> b) -> (x : Maybe (m a)) ->
    swapMaybe (map (map g) x) = map (map g) (swapMaybe x)
swapMaybePreservesMap g Nothing = ?outOfScope
swapMaybePreservesMap g (Just x) = trans
    (sym $ functorComposition x g Just)
    (functorComposition x Just (map g))

Сообщение: 

When checking right hand side of swapMaybePreservesMap with expected type
        swapMaybe (map (map g) (Just x)) = map (map g) (swapMaybe (Just x))

When checking an application of function trans:
        Type mismatch between
                map (map g . Just) x = (map (map g) . map Just) x (Type of functorComposition x Just (map g))
        and
                map (\x1 => Just (g x1)) x = map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x) (Expected type)

        Specifically:
                Type mismatch between
                        map (map g) (map Just x)
                and
                        map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)

Применение VerifiedMonad ограничения типа к swapMaybe вместо Monad делает проверку типов счастливой (с реализацией swapMaybePreservesMap сверху): 

swapMaybe : Monad m => Maybe (m a) -> m (Maybe a)
swapMaybe Nothing = pure Nothing
swapMaybe (Just x) = map Just x

Однако было бы неплохо доказать какое-либо свойство функции, работающее с некоторым Monad, которое выполняется только для VerifiedMonad.

...