В Идрисе, как добавить 1 к плавнику, пока не будет достигнут максимум

У меня есть тип данных, который принимает число в конструкторе, и это число ДОЛЖНО быть между 1 и 5 (представлено как 0..4):

import Data.Fin
data Stars = MkStars (Fin 5)

Я хочу создать функцию, которая добавляет единицу к существующему star, и если это уже 5 stars, ничего не делает

Я старался

addOneStar: Stars -> Stars
addOneStar (MkStars FZ) = MkStars (FS FZ)
addOneStar (MkStars (FS x)) = if x < 3 
                              then MkStars (FS (FS x)) 
                              else MkStars (FS x)

Но не компилируется с ошибкой:

Type mismatch between
            Fin 4 (Type of x)
    and
            Fin 3 (Expected type)

    Specifically:
            Type mismatch between
                    1
            and
                    0

Может кто-нибудь объяснить мне, почему возникает эта ошибка? И Как это исправить?


enums dependent-type idris
person Molochdaa    schedule 10.07.2016    source источник

Ответы (4)


arrow_upward
1
arrow_downward

Fin реализует интерфейс Enum, предоставляя функции-преемнику succ точно желаемую семантику, что делает реализацию addOneStar тривиальной:

addOneStar: Stars -> Stars
addOneStar (MkStars s) = MkStars $ succ s
person Anton Trunov    schedule 01.10.2016

arrow_upward
4
arrow_downward

Cactus answer объясняет проблему и дает одно из возможных решений. Однако, поскольку у нас есть зависимые типы в Idris, я бы, по крайней мере, рекламировал возможность решения, которое использует это и поэтому может рассматриваться как более идиоматичное:

nextFin : (m : Fin (S n)) -> {auto p : (toNat m) `LT` n} -> Fin (S n)
nextFin {n = Z} FZ {p} = absurd $ succNotLTEzero p
nextFin {n = Z} (FS FZ) impossible
nextFin {n = S k} FZ = FS FZ
nextFin {n = S k} (FS l) {p} = let p = fromLteSucc p in
  FS $ nextFin l

Эта функция принимает в качестве аргумента доказательство того, что данный Fin не является последним. Таким образом, вы можете быть уверены на уровне проверки типов, что программа даже не попытается поставить вам nextFin за это.

Если вы этого не хотите, а хотите что-то похожее на процитированный ответ, вы также можете использовать strengthen вместе с withправил, чтобы избежать большинства случаев:

nextFin : Fin (S n) -> Maybe $ Fin (S n)
nextFin m with (strengthen m)
  | Left k = Nothing
  | Right k = Just $ FS k
person Julian Kniephoff    schedule 14.07.2016

arrow_upward
3
arrow_downward

Тип конструктора FS равен FS : Fin n -> Fin (S n), поэтому, если у вас есть x : Fin 5, даже если вы знаете, что он меньше, чем 3 : Fin 5, его тип все еще Fin 5, поэтому вы не можете передать его FS и получить еще один Fin 5; вместо этого вы получите Fin 6.

Вы можете написать функцию nextFin : Fin n -> Maybe (Fin n), которая возвращает Nothing для наибольшего Fin; но эта функция должна перестроить новый Fin, она не может просто применить FS на самом верхнем уровне. Идея состоит в том, чтобы использовать тот факт, что FZ : Fin n либо имеет, либо не имеет преемника в зависимости от того, равно ли n 1 или больше; а преемник FS k является преемником k, завернутым в FS:

import Data.Fin

total nextFin : Fin n -> Maybe (Fin n)
nextFin {n = Z}         k      = absurd k
nextFin {n = (S Z)}     _      = Nothing
nextFin {n = (S (S n))} FZ     = Just (FS FZ)
nextFin {n = (S (S n))} (FS k) = map FS $ nextFin k
person Cactus    schedule 11.07.2016
comment
Почему бы просто не бросить Maybe? - person András Kovács; 11.07.2016
comment
@ AndrásKovács: Какой будет nextFin из последних Fin? - person Cactus; 11.07.2016
comment
Да, но это тривиально можно восстановить как fromMaybe k $ nextFin k из моего nextFin; содержит меньше информации - person Cactus; 11.07.2016

arrow_upward
0
arrow_downward

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

Вы упоминаете, что ваше число должно быть между 1 и 5. (Похоже, вы строите какую-то систему рейтинга фильмов?) Вместо того, чтобы косвенно представлять это как ограниченное натуральное число между 0 и 4, почему бы просто не перечислить небольшое число разрешенных случаев напрямую? Для этого вам не нужны зависимые типы; следующее действительно для Haskell 98.

data Stars = OneStar
           | TwoStars
           | ThreeStars
           | FourStars
           | FiveStars
           deriving (Eq, Ord, Show, Read, Bounded, Enum)

addOneStar FiveStars = FiveStars
addOneStar s = succ s
person Benjamin Hodgson♦    schedule 18.07.2016
comment
На самом деле я упростил проблему, с которой столкнулся. Ожидаемое число — не от 1 до 5, а от 1 до 50, поэтому перечислять каждый случай — не очень хорошая идея. - person Molochdaa; 18.07.2016