Я недавно решил дурачиться с коиндукцией в Агде и обнаружил, что механизм "копаттернов" довольно хрупкий. Я решил перейти к поиску и определить типы M, которые более или менее обобщают все типы соиндуктивности (оставляя в стороне коиндукцию-рекурсию). Я надеялся полностью обойти весь беспорядок в copattern, но, к моему удивлению, copatterns не способен обработать конструктор M:
{-# OPTIONS --safe #-}
module M {l}
(Index : Set l)
(Shape : Index -> Set l)
(Position : (i : Index) -> Shape i -> Set l)
(index : (i : Index) -> (s : Shape i) -> Position i s -> Index) where
record M (i : Index) : Set l where
coinductive
field shape : Shape i
field children : (p : Position i shape) -> M (index i shape p)
open M
record MBase (Rec : Index -> Set l) (i : Index) : Set l where
coinductive
field shapeB : Shape i
field childrenB : (p : Position i shapeB) -> Rec (index i shapeB p)
open MBase
unroll : (S : Index -> Set l) -> (∀ {i} -> S i -> MBase S i) -> ∀ {i} -> S i -> M i
shape (unroll S u s) = shapeB (u s)
children (unroll S u s) p = unroll S u (childrenB (u s) p)
производит:
Termination checking failed for the following functions:
unroll
Problematic calls:
shape (unroll S u s)
unroll S u (childrenB (u s) p)
Я попробовал пару небольших вариаций, но безрезультатно. Есть ли заклинание, которое заставляет безопасную Агду принять какой-либо вариант M?
Для справки, я знаю, что у меня есть несколько доступных вариантов, включая:
- включение
--sized-types и индексация M для размера - отключение
--safe и обещание компилятору, что unroll продуктивен - возможно, попробуем "коиндукцию старого стиля" ", который может или не может быть последовательным (?)
Я нахожу все это, по крайней мере, слегка неприятным, и удивлен, что ванильный сейф Agda не может справиться с этим случаем (учитывая, что это один случай, который , если обработано, оставляет пользователю аварийный люк). Я что-то упустил?