"Strictly positive" in Agda

Question

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 : ℕ -> 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.

Answer 1

HOAS doesn't work in Agda, because of this:

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

Now, notice that evaluating apply w w gives you apply w w back again. The term apply w w has no normal form, which is a no-no in agda. Using this idea and the type:

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

We can derive a contradiction.

One of the ways out of these paradoxes is only to allow strictly positive recursive types, which is what Agda and Coq choose. That means that if you declare:

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

That F must be a strictly positive functor, which means that X may never occur to the left of any arrow. So these types are strictly positive in X:

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

But these are not:

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

So in short, no you can't represent your data type in Agda. You can use de Bruijn encoding to get a term type you can work with, but usually the evaluation function needs some sort of "timeout" (generally called "fuel"), e.g. a maximum number of steps to evaluate, because Agda requires all functions to be total. Here is an example due to @gallais that uses a coinductive partiality type to accomplish this.