Я пытаюсь кодировать некоторую денотационную семантику в 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 в определении Значение.
Что это значит? Могу ли я закодировать это в Агда? Неужели я ошибаюсь?
Спасибо.