[Agda] not able to run Agda on Haskell and Emac and a relevant hypercomputing question

[Andreas Abel]

Hi Ren,

there is also the official documentation

   http://agda.readthedocs.io/en/latest/

but it is work in progress.

On 16.06.2016 20:34, Ren Rise wrote:
> Hi Andreas,
> I have visited http://learnyouanagda.liamoc.net/pages/introduction.html
> to learn about Agda programming. Subsequently I had downloaded GNU Emac
> and Haskell Compiler. But I failed to setup Agda despite following the
> instructions there at the URL. I have posted below the errors and
> exceptions WinGHCi is throwing up.
> Prelude> $ agda-mode setup

You have to run this command from the OS shell (like bash, tcsh, etc.). 
  Just type

   agda-mode setup

at the OS command line, not inside GHCI.

> <interactive>:9:1: error:
>      parse error on input ‘$’
>      Perhaps you intended to use TemplateHaskell
> Prelude>
> Prelude> :load "emacs.exe"
> target ‘emacs.exe’ is not a module name or a source file
> Prelude> $ cabal install Agda
> <interactive>:12:1: error:
>      parse error on input ‘$’
>      Perhaps you intended to use TemplateHaskell
> Prelude> TemplateHaskell
> <interactive>:13:1: error:
>      Data constructor not in scope: TemplateHaskell
> Prelude>
> Please tell me what I am doing wrong here.

> In addition to this I have a
> question. I had a chance to briefly look into your paper titled
> "Well-founded Recursion with Copatterns and Sized Types"  What are the
> implications of programming both finite and infinite structures for our
> target decidable(halting) as well as long-running non-halting apps
> running on blockchain? Does this mean it(Agda?) can support both halting
> apps such as a financial contract with definite
> expiry/expiry/redemption/maturity date/timestamp and non-halting
> long-running apps such as an online Autonomous Voice Agent and an
> automated forex trading bot simultaneously?

In Agda you can implement both provably termination programs and 
provably productive programs.  The latter means programs that respond to 
each request in finite time (provably).

There is no library yet for parallel execution (if you mean this by 
"simultaneously").  This could be overcome by some foreign function 
interface (FFI) binding to Haskell.

> I thought we can't possibly achieve this in Turing machines/digital
> computers or networks. Only futuristic SupraTuring hypercomputers and
> hypercomputing networks would be able to achieve this apparently
> impossible feat.
> I look forward to hearing from you.
> Regards,
> Ren

Cheers,
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/