Тип данных, охватывающий два типа суммы?

Учитывая эти 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?


idris
person Kevin Meredith    schedule 22.04.2016    source источник
comment
Почему бы не просто Either (Either Foo Bar) String?   -  person xash    schedule 22.04.2016

Ответы (1)


arrow_upward
3
arrow_downward

Да действительно можно!

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

person ScarletAmaranth    schedule 22.04.2016
comment
Есть ли у Idris сопутствующие продукты, согласно reddit.com/r/scala/ комментарии/4g43js/union_types_in_scala/d2fimz5? - person Kevin Meredith; 27.04.2016