数据类型包含两个和类型？

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)。