Define a data type inside an interface in Idris

Question

I wish to create a class of types for which one can prove a certain element is positive or negative, or zero. I have created an interface:

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

Now I'd like to create an implementation for Nat, but I can't work out the syntax for it. This for instance does not work:

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

I get not end of block error where data Positive stands in the implementation. Omitting data Positive... line, however, does not work either. Idris then says that method Positive is undefined. So how do I implement a type inside an interface?

Also the following does not seem to work:

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

With Idris saying: Can't find implementation for Signed phTy. So what's the correct syntax to do all this? And perhaps I'm doing it the wrong way? I'm aware of the existence of Data.So, but after a few experiments it seems complicated to me and I'd prefer to work with manually defined proofs, which is a lot simpler. Besides the doc for Data.So states itself that it should really be used with primitives.

Sventimir Sventimir · Accepted Answer · 2019-02-19T17:08:26

It seems I have figured this out eventually. This is the code that works:

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)

So in order to deliver implementation of a datatype demanded by an interface, you have to define it separately and only then say the type demanded by an interface is equal to what you've defined.

As for the type depending on the interface, you just need to specify an additional implicit argument in order to declare the type of a (unfortunately it's not possible to write Positive (a : t) -> NonZero a. You actually seem to need that implicit. Other than that it seems to work fine, so I believe that's the answer to the question. Of course any additional input from someone more learned in the ways of Idris is welcome.

Define a data type inside an interface in Idris

1 Answers