StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p><a href="http://en.wikipedia.org/wiki/Higher-order_abstract_syntax" rel="nofollow noreferrer">HOAS</a> doesn't work in Agda, because of this:</p> <pre><code>apply : Value -> Value -> Value apply (FunVal f) x = f x apply _ x = Error "Applying non-function" w : Value w = FunVal (\x -> apply x x) </code></pre> <p>Now, notice that evaluating <code>apply w w</code> gives you <code>apply w w</code> back again. The term <code>apply w w</code> has no normal form, which is a no-no in agda. Using this idea and the type:</p> <pre><code>data P : Set where MkP : (P -> Set) -> P </code></pre> <p>We can derive a contradiction.</p> <p>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:</p> <pre><code>data X : Set where MkX : F X -> X </code></pre> <p>That <code>F</code> must be a strictly positive functor, which means that <code>X</code> may never occur to the left of any arrow. So these types are strictly positive in <code>X</code>:</p> <pre><code>X * X Nat -> X X * (Nat -> X) </code></pre> <p>But these are not:</p> <pre><code>X -> Bool (X -> Nat) -> Nat -- this one is "positive", but not strictly (X * Nat) -> X </code></pre> <p>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. <a href="https://gist.github.com/gallais/303cfcfe053fbc63eb61" rel="nofollow noreferrer">Here is an example</a> due to @gallais that uses a coinductive partiality type to accomplish this.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload