Проблема в том, что у Идриса нет возможности узнать, что базовый функтор, который вы используете для своего типа данных, строго положителен.Если бы оно приняло ваше определение, вы могли бы использовать его с конкретным отрицательным функтором и доказать Void из него.
Существует два способа представления строго положительных функторов: путем определения юниверса или использованияконтейнеры.Я поместил все в две автономные гисти (но там нет комментариев).
Вселенная строго положительных функторов
Вы можете начать с базового представления: мы можем разложить функтор на сигма-тип (Sig), (строго положительную) позицию для рекурсивной субструктуры (Rec) или вообще ничего (End).Это дает нам это описание и его расшифровку как Type -> Type функцию:
-- A universe of positive functor
data Desc : Type where
Sig : (a : Type) -> (a -> Desc) -> Desc
Rec : Desc -> Desc
End : Desc
-- The decoding function
desc : Desc -> Type -> Type
desc (Sig a d) x = (v : a ** desc (d v) x)
desc (Rec d) x = (x, desc d x)
desc End x = ()
Как только у вас будет эта вселенная функторов, которые гарантируют , чтобы быть строго положительными, вы можете взять их наименьшееfixpoint:
-- The least fixpoint of such a positive functor
data Mu : Desc -> Type where
In : desc d (Mu d) -> Mu d
Теперь вы можете определить свой любимый тип данных.
Пример: Nat
Мы начнем с типа тегов суммы для каждого из конструкторов.
data NatC = ZERO | SUCC
Затем мы определяем строго положительный базовый функтор, сохраняя тег конструктора в сигме и вычисляя остальную часть описания на основе значения тега.Тег ZERO связан с End (больше ничего не нужно хранить в конструкторе zero), в то время как SUCC требует Rec End, то есть одна рекурсивная субструктура, соответствующая предшественнику Nat.
natD : Desc
natD = Sig NatC $ \ c => case c of
ZERO => End
SUCC => Rec End
Наш индуктивный тип получается, взяв фиксированную точку описания:
nat : Type
nat = Mu natD
Мы можем естественным образом восстановить ожидаемые нами конструкторы:
zero : nat
zero = In (ZERO ** ())
succ : nat -> nat
succ n = In (SUCC ** (n, ()))
Список литературы
Эта конкретная вселенная взята из «Орнаментальных алгебр, алгебраических украшений» МакБрайда, но вы можете найти более подробную информацию в «Нежном искусстве левитации» Чепмена, Даганда, МакБрайда и Морриса.
Строго положительные функторы как расширение контейнеров
Второе представление основано на другой декомпозиции: каждый индуктивный тип рассматривается как общая форма (то есть его конструкторы и данные, которые они хранят) плюс ряд рекурсивных позиций(который может зависеть от конкретного значения формы).
record Container where
constructor MkContainer
shape : Type
position : shape -> Type
Еще раз мы можем дать емуинтерпретация как Type -> Type функция:
container : Container -> Type -> Type
container (MkContainer s p) x = (v : s ** p v -> x)
И взять фиксированную точку строго положительного функтора, определенного таким образом:
data W : Container -> Type where
In : container c (W c) -> W c
Вы можете еще раз восстановить ваши любимые типы данных, определив Container s интереса.
Пример: Nat
У натуральных чисел есть два конструктора, каждый из которых ничего не хранит вообще.Таким образом, форма будет Bool.Если мы находимся в zero случае, то нет рекурсивных позиций (Void), а в succ есть ровно одна (()).
natC : Container
natC = MkContainer Bool (\ b => if b then Void else ())
Наш тип полученвзяв фиксированную точку контейнера:
nat : Type
nat = W natC
И мы можем восстановить обычные конструкторы:
zero : nat
zero = In (True ** \ v => absurd v)
succ : nat -> nat
succ n = In (False ** \ _ => n)
Ссылки
Это основано на «Контейнеры: Построение строгоПозитивные типы »Эбботта, Альтенкирх и Гани.