[Agda] Re: Agda running in the browser

[Alan Jeffrey]

Agda now knows where your (HTML5 geolocation compatible) browser is.

   http://ect.bell-labs.com/who/ajeffrey/agda-frp-js/geolocation.html

Generated from:

   main : ⟦ Beh DOM ⟧
   main =
     text ["Current location: "] ++
     text (map show geolocation) ++
     text ["."]

using a spooky postulate:

   geolocation : ⟦ Beh ⟨ Maybe Coords ⟩ ⟧

I just came back from a walk round the block with my Android phone, and 
watched my coordinates update themselves.

A.

On 09/15/2011 01:44 PM, Jeffrey, Alan S A (Alan) wrote:
> Hi everyone,
>
> I did enough mucking around with back end gore to finally get an Agda
> program running in the browser (as long as your browser supports the
> HTML5 timer model, i.e. is not I.E.). The very thrilling result is:
>
>     http://ect.bell-labs.com/who/ajeffrey/agda-frp-js/clock.html
>
> which was generated from the top-level program:
>
>     clock : ⟦ Beh DOM ⟧
>     clock = element "p" (text (map toUTCString (every (1 sec))))
>
> The source repository is here:
>
>     https://github.com/agda/agda-frp-js/
>
> although it requires some compiler patches I only just pushed, so it may
> not compile for anyone else right now.
>
> Still early days, but look! Agda! In the browser!
>
> A.