В зависимости от типизированной карты - не может быть ошибкой?

Question

Предположим, что я определяю свой собственный тип списка.

data MyVec : Nat -> Type -> Type where 
    MyNil : MyVec Z a 
    (::) : a -> MyVec k a -> MyVec (S k) a 

И myMap функция служит fmap для MyVec:

myMap : (a -> b) -> MyVec k a -> MyVec k b 
myMap f MyNil  = ?rhs_nil 
myMap f (x :: xs) = ?rhs_cons 

Попытка решить ?rhs_nil дыру в моей голове:

1. :t ?rhs_nil является MyVec 0 b
2. достаточно справедливо - я нужен конструктор t шляпа возвращается MyVec параметризовано b и мне нужно k быть 0 (или Z), и я могу видеть, что MyNil индексируется Z и параметризовано угодно, так что я могу использовать b легко, поэтому ?rhs_nil = MyNil и typechecks, денди
3. :t ?rhs_cons является MyVec (S k)
4. мне нужен конструктор, который возвращает MyVec параметризовано b и мне нужно k быть (S k)

Я вижу, что конструктор (::) строит список, проиндексированный (S k), и я пытаюсь его использовать. Первый аргумент должен быть типа b, учитывая, что я строю MyVec <> b и единственный способ получить его - применить x до f.

myMap f (x :: xs) = f x :: <>

Теперь я запутаться. RHS из (::) должна быть MyVec k b, почему я не могу просто использовать MyNil конструктор, с объединительным/замещением k == Z (тот MyNil) дает мне получать:

myMap f (x :: xs) = f x :: MyNil

Я понимаю, что мне нужно recurse и имеют = f x :: myMap f xs, но как компилятор знает, сколько раз должен использоваться конструктор (::)? Как он выводит правильный k для этого случая, не позволяя мне использовать Z.

Answer 1

k уже подразумевается xs : MyVec k a. Таким образом, вы не можете объединить k с Z, если xs содержит некоторые элементы.