«Строго положительный» в Агдии

Question

Я пытаюсь кодировать некоторую денотационную семантику в AGDA на основе программы, которую я написал в Haskell.

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

В АГДА, прямой перевод будет;

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ℕ -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

Но я получаю ошибку, относящуюся к FunVal, потому что;

Значение не строго положительно, потому что оно происходит слева от стрелки в типе конструктора FunVal в определении значения.

Что это значит? Могу ли я кодировать это в Agda? Я иду через это неправильно?

Спасибо.

Answer 1

Приманка Не работает в Agda, из-за этого:

apply : Value -> Value -> Value
apply (FunVal f) x = f x
apply _ x = Error "Applying non-function"

w : Value
w = FunVal (\x -> apply x x)

Теперь обратите внимание, что оценка apply w w дает тебе apply w w снова обратно. Период, термин apply w w не имеет нормальной формы, которая не является отсутствием в АГДА. Используя эту идею и тип:

data P : Set where
    MkP : (P -> Set) -> P

Мы можем вывести противоречие.

Одним из путей из этих парадоксов является только для того, чтобы разрешить строго положительные рекурсивные типы, в котором выбирают AGDA и CoQ. Это означает, что если вы заявляете:

data X : Set where
    MkX : F X -> X

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

X * X
Nat -> X
X * (Nat -> X)

Но это не:

X -> Bool
(X -> Nat) -> Nat  -- this one is "positive", but not strictly
(X * Nat) -> X

Так что вкратце, нет, вы не можете представлять ваш тип данных в AGDA. Вы можете использовать Conding de bruijn, чтобы получить типом срока, с которым вы можете работать, но обычно требуется функция оценки, нуждается в какой-то «тайм-аут» (обычно называемое «топливом»), например, максимальное количество шагов для оценки, потому что AGDA требует всех функций быть полным. Вот пример Благодаря @Gallais, который использует второй типовой тип частичности для достижения этого.