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

Question

假设我有这样的类型：

data Foo = Bar String | Baz | Qux String

我想要这样的功能：

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

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

我想将 get 类型签名中的 Foo 替换为指定值必须是 Bar 或 Qux 的内容。 如何表达 Foo 类型的这个子集？

Answer 1

有不止一种方法可以做到这一点，但最简单的方法可能是使 Foo 成为一个类型构造函数，它接受一个参数来指示它是否是 Foo 和 String在里面或不在里面。在这个例子中，我使用了 Bool 作为参数：

%default total

data Foo : Bool -> Type where
  Bar : String -> Foo True -- a Foo constructed with Bar will have type Foo True
  Baz : Foo False -- and a Foo constructed with Baz will have type Foo False
  Qux : String -> Foo True

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

Answer 2

我会接受 Kim Stebel 的回答（如果更改 Foo 是一个选项，正如@Eduardo Pareja Tobes 所观察到的那样），但我想展示另一种方式。您可以使用子集类型，这与依赖对相同：

total
get : (f ** Not (f = Baz)) -> String
get (f ** pf) with (f)
  get (f ** _)      | (Bar s) = s                      -- this is as before
  get (f ** contra) | Baz = void $ contra Refl         -- a contradictory case
  get (f ** _)      | (Qux s) = s                      -- this is as before

(f ** Not (f = Baz))可译为"some f of type Foo, but not Baz".

要调用 get，您需要提供 Foo 类型元素的依赖对以及它不等于 Baz 的证明，例如：

s : String
s = get (Bar "bar" ** \Refl impossible)

Answer 3

您也可以混合使用这两种方法（作者 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"

Answer 4

我将遵循 List head, for example. This is basically what 标准库中采用的方法，并使用 Dec 来证明 Foo 不是 Baz 是可判定的：

%default total

data Foo = Bar String | Baz | Qux String

data NotBaz : Foo -> Type where
  IsBar: NotBaz(Bar z)
  IsQux: NotBaz(Qux z)

Uninhabited (NotBaz Baz) where
  uninhabited _ impossible

notBaz : (f : Foo) -> Dec (NotBaz f)
notBaz Baz      = No absurd
notBaz (Bar s)  = Yes IsBar
notBaz (Qux s)  = Yes IsQux

get: (f : Foo) -> {auto ok : NotBaz f} -> String
get (Bar s) { ok = IsBar } = s
get (Qux s) { ok = IsQux } = s

s: String
s = get (Bar "bar")

对此的一些评论：

不要使用只是谓词 a -> Bool 来处理 a 的子集类型；创建一个 view 就像上面的 NotBaz 一样。有关上下文，请参阅 the Idris tutorial on views, this post, and 。
尽可能使用 Dec 而不是相等。直觉上，您将能够将 Dec 用于类型上的谓词，您可以明确地决定谓词的真实性：参见上面的 notBaz。
自动隐式参数有助于减少visual/cognitive使用站点的混乱情况

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

How can I create a function that only accepts a subset of constructors of a type?

idris