时间戳

首页 > 解决方案 > 如何在 Idris 中定义仅包含某些值组合的对类型

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

问题描述

我试图通过尝试一些超出我深度的方法来了解 Idris 中的依赖类型。如果我犯了任何愚蠢的错误，请多多包涵。

给定简单类型

data Letter = A | B | C | D

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

在实践中，给定的x : Letter和y : Letter， mklpair x y将等同于mklpair y x，但我不确定该属性是否可以或应该反映在类型中。

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

标签： idrisdependent-type

解决方案

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

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您只需要检查两种情况，而不是为每个字母检查一种情况。

推荐阅读