views:

263

answers:

1

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.

+4  A: 

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. And de Bruijn encoding won't work either if you are going to evaluate terms. You can't embed the untyped lambda calculus into Agda because it has terms without normal forms, and Agda requires all programs to be normalizing.

luqui
Thanks very much. I had an inkling about something like this but didn't entirely understand.
Jason
"the simply typed lambda calculus [...] has terms without normal forms" Is that true? I thought the simply typed lambda calculus (as opposed to the untyped lambda calculus or the more complexly typed variations of the lambda calculus) always reduces to a normal form (unless you add the fixpoint operator as a built-in), which is why it is not turing-complete.
sepp2k
sepp2k, yes, my mistake. I meant untyped, but braino'd.
luqui
@sepp2k Sorry. Still trying to get my understanding of this. By fixpoint as built-in, do you mean leaving the fixpoint operator as a non-evaluated term rather than part of the evaluation function?
Jason
@Jason: By built-in I simply mean that you can not define fixpoint as a function in the simply typed lambda-calculus (while you can in the untyped lambda calculus), so it has to be built into the language as an operator (i.e. you have a keyword `fix` and special rules to evaluate expressions using the keyword).
sepp2k