"Strictly positive" in Agda
Posted
by Jason
on Stack Overflow
See other posts from Stack Overflow
or by Jason
Published on 2010-04-06T07:44:08Z
Indexed on
2010/04/07
4:23 UTC
Read the original article
Hit count: 345
I'm trying to encode some denotational semantics into Agda based on a program I wrote in Haskell.
data Value = FunVal (Value -> Value)
| PriVal Int
| ConVal Id [Value]
| Error String
In Agda, the direct translation would be;
data Value : Set where
FunVal : (Value -> Value) -> Value
PriVal : N -> Value
ConVal : String -> List Value -> Value
Error : String -> Value
but I get an error relating to the FunVal because;
Value is not strictly positive, because it occurs to the left of an arrow in the type of the constructor FunVal in the definition of Value.
What does this mean? Can I encode this in Agda? Am I going about it the wrong way?
Thanks.
© Stack Overflow or respective owner