Idris - создавать разрешимые свойства / доказательства в целом для интерфейсов - PullRequest
Новая
       8

Idris - создавать разрешимые свойства / доказательства в целом для интерфейсов

0 голосов
/ 29 июня 2018

Можно ли создать разрешаемые свойства для интерфейсов в Idris, которые можно использовать внутри самого интерфейса?

Например - скажем, у нас есть простой интерфейс Foo и тип данных FooTypeEmpty, представляющий утверждение, что данный объект foo является «пустым» (определяется как «индексируется двумя нулями»): 

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

Можно ли присвоить методу isEmpty следующий тип?: 

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

То есть использовать FooTypeEmpty, чтобы isEmpty возвращало доказательство (или противоречие), что данный объект foo является «пустым»?

Я пробовал это с взаимным блоком, но это не проверка типов: 

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

В более общем смысле: возможно ли включить доказательства в методы интерфейса, которые являются действительными / требуются для всех реализаций?

1 Ответ

0 голосов
/ 29 июня 2018

Вы не можете получить доступ к Foo, который вы строите в его определении, который понадобится isEmpty. Интерфейсы - это просто причудливые конструкторы данных, поэтому ваш интерфейс примерно эквивалентен: 

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

Благодаря самоссылке на MkFoo в isEmpty, Foo не будет строго положительным, поэтому не полным.

Так что вам придется заранее определить тип доказательства. Просто используйте тот же аргумент типа: 

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)

Если вы хотите доказать некоторые вещи о функциях, данных интерфейсу, просто укажите их в качестве дополнительных аргументов (здесь 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

Единственная функция, которую вы не можете дать FooTypeEmpty, - это функция, которая использует само доказательство.

...