如何在 Idris 中定义仅包含某些值组合的对类型答案

【问题标题】：How to define a pair type in Idris that only holds certain combinations of values如何在 Idris 中定义仅包含某些值组合的对类型
【发布时间】：2018-05-11 03:33:28
【问题描述】：

我试图通过尝试一些超出我深度的方法来了解 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，但我不确定该属性是否可以或应该反映在类型中。

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

【问题讨论】：

标签： idris dependent-type

【解决方案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 是否彼此相邻，你将需要大约 (number of letters)^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，您只需要检查两个案例，而不是每个字母一个。

【讨论】：

【解决方案2】：

您需要的是证明这些字母是相邻的。因此，根据您对邻居的定义：

data Letter = A | B | C | D

neighbours : Letter -> Letter -> Bool
neighbours A B = True
neighbours B A = True
neighbours B C = True
neighbours C B = True
neighbours C D = True
neighbours D A = True
neighbours A D = True
neighbours _ _ = False

data LPair : Type where
  MkLPair : (x : Letter) -> (y : Letter) -> {auto prf : neighbours x y = True} -> LPair

{} 使 prf 参数隐含，而 auto 告诉 Idris 弄清楚。

【讨论】：