數據類型包含兩個和類型？

Question

鑑於這些2和類型：

data Foo = A Int | B String 
data Bar = C Int | D String 

我想定義返回Either (Foo or Bar) String功能。

所以，我試圖使：

data Higher = Foo | Bar

但它無法編譯：

*ADT> :r 
Type checking ./ADT.idr 
ADT.idr:3:6:Main.Foo is already defined 
ADT.idr:4:6:Main.Bar is already defined 

如何創建一個Higher數據類型，它由Foo或Bar？

Answer 1

是的，你的確可以！現在

data Foo = A Int | B String 
data Bar = C Int | D String 

data Higher : Type where 
    InjFoo : Foo -> Higher 
    InjBar : Bar -> Higher 

你可以做InjFoo (B "Hello")或InjBar (C 5)。