如何创建仅接受类型构造函数子集的函数？

Question

假设我有这样的类型:

data Foo = Bar String | Baz | Qux String

我希望有这样的功能:

get : Foo -> String
get (Bar s) = s
get (Qux s) = s

正如所写,这是编译,但并不是全部,因为有缺失的案例; 换句话说,get Baz被视为一个洞而不是一个没有做出类型检查的表达.

我想用Foo类型签名替换它get,指定值必须是a Bar或a Qux.我该如何表达这种Foo类型的子集？

Answer 1

您还可以混合使用这两种方法（由 Kim Stiebel 和 Anton Trunov 提出）并构建辅助数据类型。该类型OnlyBarAndQux只能用Bar和的值构造Qux。对于 idris 来说，如果调用时是这种情况，则可以自动推断证明get：

module FooMe

data Foo = Bar String | Baz | Qux String

data OnlyBarAndQux: Foo -> Type where
    BarEy: OnlyBarAndQux (Bar s)
    QuxEx: OnlyBarAndQux (Qux s)

||| get a string from a Bar or Qux
total
get: (f: Foo) -> {auto prf : OnlyBarAndQux f} -> String
get (Bar s) {prf = BarEy} = s
get (Qux s) {prf = QuxEx} = s

-- Tests

test1: get $ Bar "hello" = "hello"
test1 = Refl

test2: get $ Qux "hello" = "hello"
test2 = Refl

-- does not compile
-- test3: get $ Baz = "hello"