[Agda] Re: Agda running in the browser

[Conor McBride]

On 17 Sep 2011, at 05:27, Anthony de Almeida Lopes wrote:

>> re-implement Agda in Agda,
>
> Do we know if that's possible?

Why wouldn't it be possible? It might be tricky to write a
provably terminating typechecker for Agda, but we could certainly
model Agda typechecking as a coinductive process which we could
execute in a sufficiently liberal run-time system.

Remember, "Agda is total, so it can't be Turing Complete" is as
much nonsense as saying "Haskell is pure so it can't do IO".

It's true that the operational semantics used for partial
evaluation of open terms during typechecking will not (phew!)
execute infinitary processes in an unbounded manner, just as
the GHC inliner will not (phew!) execute your program's system
calls at compile time.

It ain't Agda-in-Agda exactly, but these posts

   http://www.e-pig.org/epilogue/?p=914
   http://www.e-pig.org/epilogue/?p=955

give an Agda implementation of typechecking Set-in-Set which
lives in a suitable monad. I give a wrapper which allows you
to run the thing for a given number of steps, even within the
Agda environment, but a real run-time system could just as
well take a chance and run it for as long as it takes.

All the best

Conor