如何創建只接受其他字段的字段？

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等，保留您的原始限制，並且Idris能夠自動推斷隱含證明條款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)等類型進行變換。像長索引列表無限互惠家庭也只能使用索引類型。