[Agda] Re: Agda running in the browser

[Alan Jeffrey]

Thanks! A paper is certainly on my to-do list.

I think I'll leave it up to someone else to re-implement Agda in Agda, 
but when they do, it'll run in the browser :-)

A.

On 09/16/2011 06:11 PM, Bengt Nordstrom wrote:
> 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
>>