Как определить тип пары в Идрисе, который содержит только определенные комбинации значений - PullRequest
Новая
       16

Как определить тип пары в Идрисе, который содержит только определенные комбинации значений

0 голосов
/ 11 мая 2018

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

Учитывая простой тип 

data Letter = A | B | C | D

Я хотел бы определить тип LPair, который содержит пару Letter, так что могут быть соединены только «соседние» буквы. Например, B может быть связан с A или C, но не D или с самим собой. Это оборачивается, поэтому A и D рассматриваются как соседи.

На практике, данные x : Letter и y : Letter, mklpair x y будут эквивалентны mklpair y x, но я не уверен, может ли это свойство или должно быть отражено в типе.

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

Ответы [ 2 ]

0 голосов
/ 11 мая 2018

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

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 говорит Идрису выяснить это.

0 голосов
/ 11 мая 2018

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

...