Как определить тип пары в 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, но я не уверен, что это свойство может или должно быть отражено в типе.

Каков наилучший способ сделать такой тип?


dependent-type idris
person Etherian    schedule 11.05.2018    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Самый простой способ — создать подмножество (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)

N.B.: Этот подход хорош и прост, но как только вы реализуете функцию, которая решает, находятся ли 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 у вас есть только два случая, которые вам нужно проверить, вместо одного для каждой буквы.

person xash    schedule 11.05.2018

arrow_upward
2
arrow_downward

Что вам нужно, так это доказательство того, что буквы являются соседними. Итак, с вашим определением соседей:

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 говорит Идрису разобраться.

person imuli    schedule 11.05.2018