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

Question

假设我有一个像这样的类型:

data Foo = Bar String | Baz | Qux String

我想要一个这样的功能:

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

如所写，这可以编译，但不是总的，因为有遗漏的情况。换句话说，get Baz被视为一个漏洞，而不是不进行类型检查的表达式。

我想用某种指定值必须是Foo或get的东西来替换Bar类型签名中的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"