7.1. Browser

7.1.1. Modules

7.1.1.1. Html

An object of type Html M describes a dom tree which the user sees in his browser window. Any interactions with the user (clicking on an element, moving the mouse, entering text, …) creates an object of type M.

A dom element consists of a node name, a list of attributes and a list of children. The elementary nodes are text nodes.

Html: Any -> Any


text {M: Any}: String -> Html M
node {M: Any}: String -> List (Attribute M) -> List (Html M) -> Html M

div {M: Any} (attrs: List Attribute) (children: List (Html M)): Html M :=
    node "div" attrs children

...

7.1.1.2. Attribute

An object of type Attribute M is an attribute of a dom node which can create a message of type M.

Attribute: Any -> Any

style {M}: String -> String -> Attribute M
    -- style "background-color" "red"

attribute {M}: String -> String -> Attribute M
    -- like domNode.setAttribute('class', 'greeting') in JS

property {M}: String -> JSValue -> Attribute M
    -- property className (string "myclass")


handler {M}: String -> Decoder (M * Bool * Bool) -> Attribute M
    {: 'Decoder' decodes the event object into a message of type 'A'
       and two booleans. The first one indicates, whether propagation
       shall be stopped. The second one indicates, whether default
       behaviour shall be prevented ('stopPropagation' and
       'preventDefault').
    :}


onClick {M} (m: M): Attribute M :=
    handler "onClick" (return m)

7.1.1.3. Command

Command: Any -> Any

pushUrl {M}: Key -> String -> Command M    -- Tasks?

7.1.1.4. Subscription

Subscription: Any -> Any

receiveMessage {M}: Decoder M -> Subscription M

7.1.1.5. Encoder

JSValue: Any


undefined: JSValue

null:   JSValue

int:    JSValue

float:  JSValue

string: JSValue

bool:   JSValue

object: List (String * JSValue) -> JSValue
    -- with duplicate keys the last wins.

list:  List JSValue -> JSValue

7.1.1.6. Decoder

An object of type Decoder A decodes a javascript object into and object of type Maybe A.

Decoder (A: Any): Any :=
    JSValue -> Maybe A

return {A}: A -> Decoder A

fail {A}: Decoder A

(>>=) {A B}: Decoder A -> (A -> Decoder B) -> Decoder B

string: Decoder String

int:    Decoder Int

float:  Decoder Float

field {A}: String -> Decoder A -> Decoder A

list {A}: Decoder A -> Decoder (List A)

array {A}: Decoder A -> Decoder (Array A)

This definition has the disadvantage that it cannot handle arbitrarily deep javascript objects. In order to do that we need a parser like object.

Parser (A: Any) (i: Progress): Any :=
    JSValue -> Maybe A * JSValue

run {A i} (d: Parser A i) (v: JSValue): Maybe A :=
    match d v case
        \ (nothing, _) :=
            nothing
        \ (just a, _) :=
            just a


return {A}: A -> Parser A no

fail {A}:   Parser A no

(>>=) {A B} (m: Parser A i) (f: A -> Parser B j): Parser B (i or j) :=
    \ v :=
        match m v case
            \ (just a, v2) :=
                f a v2
            \ (nothing, v2) :=
                (nothing, v2)

string: Parser String no
int:    Parser Int    no

field: String -> Parser Unit yes        -- enters the field of an object

arrayLength: Parser Nat no

get: Nat -> Parser Unit yet             -- enters an element of an array

list {A i}: Parser A i -> Parser (List A) no

7.1.2. Browser Programs

7.1.2.1. Sandbox

A sandbox program occupies the whole browser window (i.e. it is rendered directly below the body node). The user can interact with the program by clicking of element, moving the mouse, entering text etc. The only effect of the user interaction is changing the dom.

A sandbox program cannot interact with the outside world. There are no http requests, no sending and receiving of messages from and to the outer javascript code.

Html: Any -> Any

Browser: Any                -- type for browser programs

sandbox {S M: Any}: S -> (M -> S -> S) -> (S -> Html M) -> Browser
    -- sandbox init update view

An example of a sandbox program:

use
    alba.core.int
    alba.core.string
    alba.browser.browser

type Message := [increment, decrement]

update: Mesage -> Int -> Int := case
    \ increment, i :=
        i + 1
    \ decrement, i :=
        i - 1

view: (i: Int): Html Message :=
    div []
        [   button [onClick decrement] [text "-"]
            , div [] [text (toString i)]
            , button [onClick increment] [text "+"]
        ]

7.1.2.2. Element

An element program manages only the dom subtree of an existing node of the dom. No dom elements outside the root element are neither accessible nor changeable.

An element program can interact with the surrounding javascript code by sending and receiving messages. It can make http requests. It can subscribe to external events like timers etc.

element {S M: Any}:
    Decoder (S * Command M)     -- initialisation
    ->
    (M -> S -> S * Command M)   -- update
    ->
    (S -> Html M)               -- view
    ->
    (S -> Subscription M)       -- subscriptions
    ->
    Browser

7.1.2.3. Document

A document application occupies the whole browser page and its title.

document {S M: Any}:
    Decoder (S * Command M)         -- initialisation
    ->
    (M -> S -> S * Command M)       -- update
    ->
    (S -> String * List (Html M))   -- view with title
    ->
    (S -> Subscription M)           -- subscriptions
    ->
    Browser

7.1.2.4. Single Page Application

application {S M: Any}:
    Decoder (Key -> Url -> S * Command M)       -- initialisation
    ->
    (M -> S -> S * Command M)                   -- update
    ->
    (S -> String * List (Html M))               -- view with title
    ->
    (S -> Subscription M)                       -- subscriptions
    ->
    (UrlRequest -> M)                           {: The user has clicked on a
                                                   link :}
    ->
    (Url -> M)                                  {: Forward or backward
                                                   movement in the history
                                                   without changing the main
                                                   page :}
    ->
    Browser