Как создать поле, которое принимает только другие поля?

Question

Я хочу создать тип данных с чередующимися конструкторами Foo и Bar. Действительный член, к примеру, был бы:

Foo (Bar (Foo (Bar End))) 

Но нет:

Foo (Foo (Bar End)) 

Поскольку последний имеет два последовательных Foo-х. Каков правильный способ выразить это в одной декларации данных?

Answer 1

Одно из возможных решений с использованием индексного типа:

data FooBarEnd : Nat -> Type where 
    End : FooBarEnd 0 
    Foo : FooBarEnd 1 -> FooBarEnd 0 
    Bar : FooBarEnd 0 -> FooBarEnd 1 

Пару тестов:

test1 : FooBarEnd 0 
test1 = Foo (Bar (Foo (Bar End))) 

test2 : FooBarEnd 0 
test2 = End 

test3 : FooBarEnd 1 
test3 = Bar End 

Foo (Foo (Bar End)) не является правильным термином ни для FooBarEnd 0, ни FooBarEnd 1.

Недостатком этого подхода является необходимость использования индексов 0 и 1. Я не уверен, что это то решение, которое вы ищете.

---

Если вы решили разрешить Foo End в качестве действительного члена, определение может быть изменено в этом:

data FooBarEnd : Nat -> Type where 
    End : FooBarEnd 1 
    Foo : {auto prf : n `GTE` 1} -> FooBarEnd n -> FooBarEnd 0 
    Bar : {auto prf : n `LTE` 1} -> FooBarEnd n -> FooBarEnd 2 

Где GTE и LTE означают больше или равно и меньше или равны соответственно.

выше позволяет Foo End, Bar End и т.д., сохраняя исходное ограничение, и Идрис способен выводя неявные условия доказательства prf автоматически.

Более неформально, то (унарный) конструктор Foo ожидает значение типов FooBarEnd 1 или FooBarEnd 2 в качестве аргумента, что означает, что мы только позволили построить Foo End или Foo (Bar ...), потому что мы отделили каждого из конструкторов в свой собственный «подтип» , индексированный натуральным числом. И конструктор Bar ожидает либо End (с индексом 1 < = 1) или Foo (с индексом 0 < = 1).

Answer 2

С одной декларации необходимо индексированный тип:

data Foo : Bool -> Type where 
    End : Foo True 
    Bar : Foo True -> Foo False 
    Foo : Foo False -> Foo True 

Это имеет те же жителей, как в следующих двух взаимных типов:

data FooTrue = End | Foo FooFalse 
data FooFalse = Bar FooTrue 

В общем, взаимное семейство n данных типы представляются с одним типом семейства, индексированным типом с элементами n. Индексированное представление имеет то преимущество, что оно допускает общие операции, которые невозможны с взаимными типами, поскольку могут иметь преобразования с типами {b : Bool} -> Foo b -> Foo b или {b : Bool} -> Foo b -> Foo (not b). Бесконечные взаимные семейства, такие как списки с индексацией по длине, также возможны только с индексированными типами.