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

Я пытаюсь кодировать некоторую денотационную семантику в 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 в определении Значение.

Что это значит? Могу ли я закодировать это в Агда? Неужели я ошибаюсь?

Спасибо.

Ответы

Ответ 1

HOAS не работает в 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 не имеет нормальной формы, что нет-нет в agda. Используя эту идею и тип:

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

Мы можем получить противоречие.

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

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. И кодировка de Bruijn не будет работать, если вы собираетесь оценивать условия. Вы не можете внедрить нетипизированное лямбда-исчисление в Agda, потому что оно имеет термины без нормальных форм, и Agda требует, чтобы все программы нормализовались.