Как сопоставить все целые числа в диапазоне в общей функции? - PullRequest
Новая
       58

Как сопоставить все целые числа в диапазоне в общей функции?

2 голосов
/ 30 мая 2020

Допустим, мы хотим проверить четность Int: 

data Parity = Even | Odd

Это было бы довольно просто для Nat: 

parity0: Nat -> Parity
parity0 Z = Even
parity0 (S k) = case parity0 k of
  Even => Odd
  Odd => Even

Первая попытка реализовать что для Int: 

parity1: Int -> Parity
parity1 x = if mod x 2 == 0 then Even else Odd

Эта функция не является полной:

Main.parity1, возможно, не является полным из-за: Prelude.Interfaces.Int реализации Prelude.Interfaces .Integral

Это имеет смысл, потому что mod не является общим для Int. (Хотя я не уверен, откуда я мог это знать заранее. REPL показывает, что mod всего. Очевидно, вы можете использовать частичную функцию для реализации полной функции интерфейса? Странно.)

Затем я пытаюсь использовать DivBy view: 

parity2: Int -> Parity
parity2 x with (divides x 2)
  parity2 ((2 * div) + rem) | (DivBy prf) =
    if rem == 0 then Even else Odd

Эта функция работает и является полной, но реализация подвержена ошибкам и не масштабируется до случаев, когда у нас есть несколько возможных значений. Я хотел бы заявить, что rem может быть только 0 или 1. Поэтому я пытаюсь использовать case на rem: 

parity3: Int -> Parity
parity3 x with (divides x 2)
  parity3 ((2 * div) + rem) | (DivBy prf) = case rem of
    0 => Even
    1 => Odd

Эта функция также работает, но не полностью. Как я могу использовать prf, предоставленный DivBy, чтобы убедить компилятор в том, что он полный? Как я могу использовать этот prf в целом?

Может ли использование Integer или другого типа упростить решение этой проблемы?

И есть еще одна очень важная вещь. Я попытался разделить регистр на prf и обнаружил, что следующая функция является общей: 

parity4: Int -> Parity
parity4 x with (divides x 2)
  parity4 ((2 * div) + rem) | (DivBy prf) impossible

Это ошибка? Я могу использовать эту функцию для создания кода времени выполнения sh в программе, которая содержит только общие функции.

...