Полиморфная константа в сигнатуре зависимого типа? - PullRequest
Новая
       30

Полиморфная константа в сигнатуре зависимого типа?

0 голосов
/ 09 марта 2019

Скажем, я хотел бы определить тип доказательства того, что некоторый вектор имеет определенную сумму. Я также хотел бы, чтобы это доказательство работало для любого Monoid типа t. Моя первая попытка была такой: 

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum Prelude.Algebra.neutral []
    Component : Monoid t => (x : t) -> HasSum sum xs -> HasSum (x <+> sum) (x :: xs)

К сожалению, компилятор утверждает, что Can't find implementation for Monoid t. Поэтому я попытался с неявным аргументом, чтобы я мог указать его тип: 

    EndNeutral : Monoid t => {Prelude.Algebra.neutral : t} -> HasSum Prelude.Algebra.neutral []

Это компилируется, но это не так: 

x : HasSum 0 []
x = EndNeutral

странно утверждает, что это Can't find implementation for Monoid Integer.

Моя последняя попытка состояла в том, чтобы определить вспомогательную константу с именем заглавной буквы, чтобы Идрис не перепутал ее с связанной переменной: 

ZERO : Monoid t => t
ZERO = neutral

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum ZERO []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

но теперь он не может угадать тип ZERO в определении EndNeutral (Can't find implementation for Monoid t). Поэтому я попробовал еще раз с неявной привязкой: 

    EndNeutral : Monoid t => {ZERO : t} -> HasSum ZERO []

, но теперь ZERO становится связанной переменной и, хотя она компилируется, она не работает должным образом, поскольку позволяет построить доказательство пустой векторной записи, имеющей произвольную сумму.

В этот момент у меня кончились идеи. Кто-нибудь знает, как выразить полиморфную константу в типе Идриса?

1 Ответ

0 голосов
/ 10 марта 2019

Кажется, я наконец нашел ответ.Возможно, он не самый лучший, но я знаю только об этом сейчас.Поэтому требуется явно указать тип neutral без добавления неявного аргумента (который превратит neutral в связанную переменную).Конечно, функция the может служить этой цели: 

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum (the t Prelude.Algebra.neutral) []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

edit:

Взгляд на тип neutral предлагает еще одно решение: 

> :doc neutral
Prelude.Algebra.neutral : Monoid ty => ty

Похоже, конкретный тип neutral на самом деле является неявным аргументом.Поэтому: 

EndNeutral : Monoid t => HasSum (Prelude.Algebra.neutral {ty = t}) []

также работает.

...