Определите тип данных внутри интерфейса в Idris - PullRequest
Новая
       47

Определите тип данных внутри интерфейса в Idris

0 голосов
/ 19 февраля 2019

Я хочу создать класс типов, для которого можно доказать, что определенный элемент является положительным, отрицательным или нулевым.Я создал интерфейс: 

interface Signed t where
    data Positive : t -> Type
    data Negative : t -> type
    data IsZero : t -> Type

Теперь я хотел бы создать реализацию для Nat, но я не могу определить синтаксис для него.Это, например, не работает: 

Signed Nat where
    data Positive : Nat -> Type where
        PosNat : (n : Nat) -> Positive (S n)
    data Negative : Nat -> Type where
        NegNat : Void -> Negative Nat
    data IsZero : Nat -> Type 
        ZZero : IsZero Z

Я получаю not end of block ошибку, где data Positive стоит в реализации.Однако пропуск строки data Positive... также не работает.Идрис говорит, что method Positive is undefined.Итак, как мне реализовать тип внутри интерфейса?

Также, похоже, не работает следующее: 

data NonZero : Signed t => (a : t) -> Type where
    PositiveNonZero : Signed t => Positive a -> NonZero a
    NegativeNonZero : Signed t => Negative a -> NonZero a

Со словами Идриса: Can't find implementation for Signed phTy.Так какой же правильный синтаксис для всего этого?И, возможно, я делаю это неправильно?Я знаю о существовании Data.So, но после нескольких экспериментов мне это кажется сложным, и я бы предпочел работать с определенными вручную доказательствами, что намного проще.Кроме того, документ для Data.So утверждает, что он действительно должен использоваться с примитивами.

1 Ответ

0 голосов
/ 19 февраля 2019

Кажется, я понял это в конце концов.Вот код, который работает: 

interface Signed t where
    data Positive : t -> Type
    data Negative : t -> Type
    data IsZero : t -> Type

data NonZero : t -> Type where
    PositiveNonZero : Signed t => {a : t} -> Positive a -> NonZero a
    NegativeNonZero : Signed t => {a : t} -> Negative a -> NonZero a


data PositNat : Nat -> Type where
    PN : (n : Nat) -> PositNat (S n)

data NegatNat : Nat -> Type where
    NN : Void -> NegatNat n

data ZeroNat : Nat -> Type where
    ZN : ZeroNat Z

Signed Nat where
    Positive n = PositNat n
    Negative n = NegatNat n
    IsZero = ZeroNat


oneNonZero : NonZero (S Z)
oneNonZero = PositiveNonZero (PN 0)

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

Что касается типа, зависящего от интерфейса, вам просто нужно указать дополнительный неявный аргумент, чтобы объявить тип a (к сожалению, невозможно написать Positive (a : t) -> NonZero a.Кажется, вам действительно нужен этот неявный характер. Кроме того, он, кажется, работает нормально, поэтому я считаю, что это ответ на вопрос. Конечно, приветствуется любая дополнительная информация от кого-то, более опытного в способах Идриса.

...