“Строго положительный” в Agda
Я пытаюсь закодировать некоторую денотационную семантику в Agda на основе программы, которую я записал в Haskell.
data Value = FunVal (Value -> Value)
| PriVal Int
| ConVal Id [Value]
| Error String
В Agda прямой перевод был бы;
data Value : Set where
FunVal : (Value -> Value) -> Value
PriVal : ℕ -> Value
ConVal : String -> List Value -> Value
Error : String -> Value
но я получаю ошибку, касающуюся FunVal потому что;
Значение не строго положительно, потому что оно происходит слева от стрелки в типе конструктора FunVal в определении Значения.
Что это означает? Я могу закодировать это в Agda? Я иду об этом неправильным путем?
Спасибо.
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 ww дает вам снова примените ww . Термин apply w w не имеет нормальной формы, которая является запретом в agda. Используя эту идею и тип:
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. Вы можете использовать кодировку де Брюйна, чтобы получить тип термина, с которым вы можете работать, но обычно для функции оценки требуется какой-то «тайм-аут» (обычно называемый «топливо»), например максимальное количество шагов для оценки, потому что Agda требует, чтобы все функции были полными. Вот пример из-за @gallais, который использует для этого тип коиндуктивной пристрастности.