[Agda] Re: Agda running in the browser

[Bengt Nordstrom]

Very impressive Alan! Hope you will write a paper about it.

Now we can start to hope for an editor of a dependently typed language
in our browser.

-- Bengt

On Sat, Sep 17, 2011 at 5:40 AM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>