Какие индуктивные схемы могут закодировать следующее определение Агда?

Question

Какие индукционные схемы (напр.индукция-рекурсия Дюбьера и Сетцера, «ирландская» индукция-рекурсия Макбрайда или индукция-индукция Форсберга и Сетцера или, возможно, некоторые более простые) позволяют закодировать следующее определение Агда

  data A : Set where
    a : Maybe (List A) → A

Я могу придумать несколько приемов, чтобы переформулировать List в этом определении, так что индукция-рекурсия становится применимой, но существуют ли какие-либо схемы, которые позволили бы мне сначала сказать, что такое список, а затем обратиться к этой информации, чтобы сказать, что A так это делается в Агде?

Редактировать:Как следует из ответа Андраша Ковача, это особый определение можно переформулировать как индуктивное семейство.Вот как это сделать:

data Three : Set where one two three : Three

data AG : Three → Set where
  a'       : AG three → AG one
  nil'     : AG two
  cons'    : AG one → AG two → AG two
  nothing' : AG three
  just'    : AG two → AG three

A = AG one
ListA = AG two
MaybeListA = AG three

a : MaybeListA → A
a = a'

nil : ListA
nil = nil'

cons : A → ListA → ListA
cons = cons'

nothing : MaybeListA
nothing = nothing'

just : ListA → MaybeListA
just = just'

Answer 1

Ни одна известная мне схема не кодирует этот тип напрямую.Иногда это называют «вложенным» индуктивным определением.Сложность здесь в том, что Maybe и List являются конструкторами типов, внешними по отношению к сигнатуре, и нам необходимо формализовать строгую позитивность для операторов внешних типов в целом, если мы хотим разрешить такие определения.

Другими словами, согласованность A зависит от определения Maybe и List.Некоторые операторы внешнего типа не являются положительными, например:

data Neg (A : Set) : Set where
  neg : (A -> Bool) -> Neg A

data B : Set where
  b : Neg B -> B

Agda просматривает все внешние определения и пытается определить дисперсию параметров типа.Хотя я не знаю ссылки на прямую формальную спецификацию этого, простой способ переформулировать вложенные определения как невложенные — включить операторы внешнего типа во взаимную индуктивную сигнатуру.Например:

data A : Set 
data ListA : Set
data MaybeListA : Set

data A where
  a : MaybeListA -> A

data ListA where
  nil : ListA
  cons : A -> ListA -> ListA

data MaybeListA where
  nothing : MaybeListA
  just : ListA -> MaybeListA

Это обычный тип взаимной индуктивности, который покрывается (по модулю косметических деталей) индуктивными семействами Дюбьера.