Idris - create decidable properties/ proofs in general for interfaces

Question

Is it possible to create decidable properties for interfaces in Idris that can be used within the interface itself ?

For example - let's say we have a simple interface Foo and a datatype FooTypeEmpty representing a statement that a given foo object is 'empty ' (defined as 'is indexed by two zeros'):

interface Foo (foo : Nat -> Nat -> Type -> Type) where
    mkEmpty : foo 0 0 a
    isEmpty : (f : foo n m a) -> Bool

data FooTypeEmpty : (Foo foo) => foo n m a -> Type where
    MkFooTypeEmpty : (Foo foo) => (f : foo 0 0 a) -> FooTypeEmpty f 

Is it possible to give the isEmpty method the following type ?:

isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty f)

That is, make use of FooTypeEmpty so that isEmpty returns a proof (or contradiction) that the given foo object is 'empty' ?

I tried it with a mutual block, but this won't typecheck:

mutual
    interface Foo (foo : Nat -> Nat -> Type -> Type) where
        mkEmpty : foo 0 0 a
        isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty f)

    data FooTypeEmpty : (Foo foo) => foo n m a -> Type where
        FTE : (Foo foo) => (f : foo 0 0 a) -> FooTypeEmpty f

More generally : Is it possible to incorporate proofs in interface methods that are valid/required for all implementations ?

Answer 1

You can't access the Foo you are constructing in his definition, which would be needed by isEmpty. Interfaces are just fancy data constructors, so your interface is roughly equivalent to:

MkFoo : (foo : Nat -> Nat -> Type -> Type) ->
        (mkEmpty : foo 0 0 a) ->
        (isEmpty : ((f : foo n m a) -> 
            Dec (FooTypeEmpty f {Foo interface=MkFoo foo mkEmpty isEmpty})) ->
        Foo foo

Thanks to the self-reference to MkFoo in isEmpty, Foo wouldn't be strictly positive, therefore not total.

So you would have to define the proof type beforehand. Just use the same type argument:

data FooTypeEmpty : {foo : Nat -> Nat -> Type -> Type} -> 
                    foo n m a -> Type where
    FTE : {foo : Nat -> Nat -> Type -> Type} ->
          (f : foo 0 0 a) -> FooTypeEmpty f

interface Foo (foo : Nat -> Nat -> Type -> Type) where
    mkEmpty : foo 0 0 a
    isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty f)

data Bar : Nat -> Nat -> Type -> Type where
  Empty : Bar 0 0 a

Foo Bar where
  mkEmpty = Empty
  isEmpty = \Empty => Yes (FTE Empty)

If you want to prove some things about the functions given to the interface, just give them as extra arguments (here mkEmpty):

data FooTypeEmpty : {foo : Nat -> Nat -> Type -> Type} -> 
                    {mkEmpty : foo 0 0 a} ->
                    foo n m a -> Type where
    FTE : {foo : Nat -> Nat -> Type -> Type} ->
          {mkEmpty : foo 0 0 a} ->
          FooTypeEmpty mkEmpty

interface Foo (foo : Nat -> Nat -> Type -> Type) where
    mkEmpty : foo 0 0 a
    isEmpty : (f : foo n m a) -> Dec (FooTypeEmpty {mkEmpty} f)

data Bar : Nat -> Nat -> Type -> Type where
  Empty : Bar 0 0 a

Foo Bar where
  mkEmpty = Empty
  isEmpty = \Empty => Yes FTE

The only function you can't give to FooTypeEmpty is the function that uses the proof itself.