несоответствие типов происходит при равных оценочных значениях - PullRequest
Новая
       46

несоответствие типов происходит при равных оценочных значениях

1 голос
/ 28 сентября 2019

Я новичок в Idris и пытаюсь сделать код действительным.

Не могли бы вы дать мне лучшее место для вопросов о нубах по Idris? 

filter : (elem -> Bool) -> Vect len elem -> (p: (Fin len) ** Vect (finToNat p) elem)
filter {len=S l} p xs = ((FZ {k=l}) ** [])
filter {len=S l} p (x::xs) =
  let (a ** tail) = filter {len=l} p xs
   in if p x then
        ((FS a) ** x::tail)
      else
        ((weaken a) ** tail)

Я написал еще один filter, который еще не может пройти проверку типа.

Этот новый тип filter подразумевает, что отфильтрованный вектор не может быть длиннее исходного.

Однако Идрис сказал: 

...
Specifically:
                Type mismatch between
                        finToNat a
                and
                        finToNat (weaken a)

Мы знаем, что эти два термина всегда имеют одно и то же значение.

Как я могу описать этот факт и позволить Идрису сказать «хорошо»?

1 Ответ

0 голосов
/ 28 сентября 2019

Вы должны показать, что finToNat a = finToNat (weaken a).tail имеет тип Vect (finToNat a) elem, но вам нужно Vect (finToNat (weaken a)) elem для второго компонента в последней строке, потому что вы написали weaken a в первом компоненте пары. 

lemma : {n : _} -> (a : Fin n) -> finToNat (weaken a) = finToNat a
lemma FZ     = Refl
lemma (FS x) = rewrite lemma x in Refl

filter : (elem -> Bool) -> Vect len elem -> (p: (Fin len) ** Vect (finToNat p) elem)
filter {len=S l} p xs = ((FZ {k=l}) ** [])
filter {len=S l} p (x::xs) =
  let (a ** tail) = Main.filter {len=l} p xs
  in if p x then
       ((FS a) ** x::tail)
     else
       (weaken a ** (rewrite lemma a in tail))
...