idris - 如何在 Idris 中定义仅保存某些值组合的对类型

Question

我正在尝试通过超出我的深度的方式来了解 Idris 中的依赖类型。如果我犯了任何愚蠢的错误，请容忍我。

给定简单类型

data Letter = A | B | C | D

我想定义一个类型LPair，它包含一对Letter，这样只有“相邻”字母可以配对。例如，B 可以与 A 或 C 配对，但不能与 D 或其本身配对。它环绕，因此 A 和 D 被视为邻居。

实际上，给定 x : Letter 和 y : Letter，mklpair x y 将相当于 mklpair y x >，但我不确定该属性是否可以或应该反射(reflect)在类型中。

制作这种类型的最佳方法是什么？

Answer 1

最直接的方法是创建 (Letter, Letter) 的子集，其中元素满足谓词 (a, b : Letter) -> Either (Next a b) (Next b a )，其中 Next 只是右侧的邻居:

data Letter = A | B | C | D

data Next : Letter -> Letter -> Type where
  AB : Next A B
  BC : Next B C
  CD : Next C D
  DA : Next D A

Neighbour : Letter -> Letter -> Type
Neighbour a b = Either (Next a b) (Next b a)

LPair : Type
LPair = (p : (Letter, Letter) ** Neighbour (fst p) (snd p))

mklpair : (a : Letter) -> (b : Letter) -> {auto prf : Neighbour a b} -> LPair
mklpair a b {prf} = ((a, b) ** prf)

<小时/>

注意:这种方法很好也很简单，但是一旦你实现了一个函数来决定 a 和 b 是否彼此相邻，你将需要 (字母数)^3情况:

isNext : (a : Letter) -> (b : Letter) -> Dec (Next a b)
isNext A A = No nAA where
  nAA : Next A A -> Void
  nAA AB impossible
  nAA BC impossible
  nAA CD impossible
  nAA DA impossible
isNext A B = Yes AB
...

如果您有很多字母并且需要决策函数，通常的方法是将数据映射到递归类型，例如 Nat。由于您的模数大小写 (Next D A)，您需要一个如下包装器:

data NextN : Nat -> Nat -> Nat -> Type where
  NextS : {auto prf :      (S a) `LTE` m}  -> NextN m a (S a) -- succ in mod m
  NextZ : {auto prf : Not ((S a) `LTE` m)} -> NextN m a Z     -- wrap around

LToN : Letter -> Nat
LToN A = 0
LToN B = 1
LToN C = 2
LToN D = 3

LNeighbour : Letter -> Letter -> Type
LNeighbour x y =
  let a = LToN x
      b = LToN y
  in Either (NextN 3 a b) (NextN 3 b a)

LNPair : Type
LNPair = (p : (Letter, Letter) ** LNeighbour (fst p) (snd p))

mklnpair : (a : Letter) -> (b : Letter) -> {auto prf : LNeighbour a b} -> LNPair
mklnpair a b {prf} = ((a, b) ** prf)

使用 NextS 和 NextZ，您只需检查两个案例，而不是每个字母一个。