[Agda] Re: Agda running in the browser

[Alan Jeffrey]

So now Agda lets you press buttons:

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

The source is:

   main = text lab ++ but where
     but = element "button" (text ["OK"])
     lab = hold "Press me: " (tag "Pressed: " (listen click but))

The important part being "listen click but" which produces a stream of 
events from the "but" element. The code "hold X (tag Y Z)" is 
boilerplate code for a behaviour that starts out with value X and 
switches to value Y when Z fires an event.

This took a while to work out the API for. Ideas I ended up not using 
were a) implementing pi-calculus-style channels (or some similar 
nu-calculus-style trickery with name generation), b) treating event 
streams as nondeterministic, and using a linear type system a la 
Krishnaswami and Benton's ICFP 2011 paper, and c) an Int-construction 
for building a closed (para)category out of a (partial) trace a la 
Malherbe, Scott and Selinger.

In each case the reason I abandoned it was that it means moving away 
from the pure language (where arrows are functions and products are 
pairs) and into the Kleisli category of a monad, or some other symmetric 
monoidal category. In Haskell terms, this is trying to avoid using 
monads or arrows.

What I ended up using was parameterizing DOM object types by location. 
So the type for a DOM object is (DOM w), and w stands for where in the 
DOM tree the object lives (i.e. a path from the root element).  Some of 
the primitives (OK, with a bit of simplification to ignore the temporal 
aspects) are:

   DOW : Set // "Upside-down DOMs", aka Document Object Worlds
   DOM : DOW -> Set
   EventType : Set -> Set
   Mouse : Set
   click : EventType Mouse
   events : {A : Set} -> EventType A -> DOW -> Evt A

Note that the primitive for event streams is parameterized on a 
location, not a DOM object. The function "listen" is then definable:

   listen : {A : Set} {w : DOW} -> EventType A -> DOM w -> Evt A
   listen {A} {w} t d = events t w

The functions which build DOMs then infer DOWs top-down, for example 
(again, ignoring the temporal aspects):

   left right : DOW -> DOW
   _++_ : {w : DOW} -> DOM (left w) -> DOM (right w) -> DOM w

In the opening example, "but" ends up with type "DOM (right w)", and so 
"listen click but" expands to "events click (right w)".

OK, there are some gotchas with the semantics, the most notable being:

   listen t (if false then foo else bar) === listen t foo

since foo and bar must have the same type (DOM w) and so both sides 
beta-reduce to (events t w). But (as far as I know) this is the first 
such event model which is completely pure (no name generation, 
nondeterminism, monads, arrows, etc. etc.)

Phew, that was a lot of work just to get a button press to work.

A.

On 09/16/2011 03:40 PM, Jeffrey, Alan S A (Alan) 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.