browser.dom

For the page’s DOM: its operations, each taking the evidence that the DOM is in the program’s effect (as state’s get does). heff compile --backend=page compiles a computation of this world — Co dom Unit, or a sum of worlds — to a script for a page, each world’s algebra from its provider.

import co
import browser.dom

greeting : String -> String
greeting name = if name == "" then "Hello, whoever you are." else "Hello, " ^ name ^ "!"

-- | the paragraph greets whatever is typed into the input
greeter : {e : HFunctor} -> {{page : dom <: e}} -> Co e Unit
greeter = do
  with withDocument as doc do
    out <- xpath doc "//p[@id='greeting']"
    name <- select doc "#name"
    found out (\o -> do
      text o (greeting "")
      found name (\n -> on n "input" (\v -> text o (greeting v))))

The page’s document is had by withDocument, at the top of the program, as a With s Document: what finds and makes elements (select, xpath, create) takes it. An element is the host’s own, a foreign value, passed by value: to the operations on it here (text, attr, append, on), and to another effect’s — a <canvas> found here, drawn on by a GPU’s effect inside the same with. The page owns its elements, so there is nothing to let go of: an element the program drops is the collector’s. An app only gets elements from the operations — it makes them, or finds them on the page: where one goes on the page is the app’s to say.

Document

data Document

The page’s document: the host’s own, had as a With s Document by withDocument’s body.

Element

data Element

An element of the page: the host’s own, passed by value.

DomF

data DomF (m : Type -> Type) x
  = Open (Document -> x)
  | Close Document x
  | Create Document String (Element -> x)
  | Text Element String x
  | Attr Element String String x
  | Append Element Element x
  | Clear Element x
  | Value Element (String -> x)
  | On Element String (String -> m Unit) x
  | Same Element Element (Bool -> x)
  | Select Document String (Maybe Element -> x)
  | XPath Document String (Maybe Element -> x)
  | Sleep Int x
  | Fetch String (String -> x)

dom

dom : HFunctor

For the page’s document: elements found and made, their text, attributes and children set, a field’s value read, events handled; and a wait, and a URL fetched.

withDocument

withDocument : {e : HFunctor}
             -> {a : Type}
             -> {{ev : dom <: e}}
             -> {{cu : custodian <: e}}
             -> ({s : Type} -> With s Document -> Co e a)
             -> Co e a

The page’s document, held by body in a region of its own, and let go of as the block is left: what it came to. A page always has its document, so nothing is thrown. Letting go of it closes nothing: the document is the page’s, which keeps it, and the program has it still where it gave it on — to a handler set on an element, run after the block; to another effect, by value. A program has its page once, at the top, and finds and makes its elements inside.

create

create : {e : HFunctor}
       -> {s : Type}
       -> {{ev : dom <: e}}
       -> With s Document
       -> String
       -> Co e Element

An element made, of the tag: on no page until it is appended.

text

text : {e : HFunctor} -> {{ev : dom <: e}} -> Element -> String -> Co e Unit

The element’s text set: all it holds, as text.

attr

attr : {e : HFunctor}
     -> {{ev : dom <: e}}
     -> Element
     -> String
     -> String
     -> Co e Unit

The element’s attribute a set to v.

append

append : {e : HFunctor} -> {{ev : dom <: e}} -> Element -> Element -> Co e Unit

The child appended to the parent, as its last.

clear

clear : {e : HFunctor} -> {{ev : dom <: e}} -> Element -> Co e Unit

The element’s children, all removed.

value

value : {e : HFunctor} -> {{ev : dom <: e}} -> Element -> Co e String

An input’s value, as it is now.

on

on : {e : HFunctor}
   -> {{ev : dom <: e}}
   -> Element
   -> String
   -> (String -> Co e Unit)
   -> Co e Unit

The handler run at each of the element’s events of the name ("input", "click"), given the value of what it happened to ("" where that has none).

same

same : {e : HFunctor} -> {{ev : dom <: e}} -> Element -> Element -> Co e Bool

Whether two elements are one: the same element of the page, found twice, say.

select

select : {e : HFunctor}
       -> {s : Type}
       -> {{ev : dom <: e}}
       -> With s Document
       -> String
       -> Co e (Maybe Element)

The first element of the page a CSS selector matches (#out, ul > li.done), if one does.

xpath

xpath : {e : HFunctor}
      -> {s : Type}
      -> {{ev : dom <: e}}
      -> With s Document
      -> String
      -> Co e (Maybe Element)

The first element of the page an XPath matches (//button[text()='Go']), if one does.

found

found : {e : HFunctor} -> Maybe Element -> (Element -> Co e Unit) -> Co e Unit

Go on with an element, if it was found.

sleep

sleep : {e : HFunctor} -> {{ev : dom <: e}} -> Int -> Co e Unit

Wait: in the page, the rest runs when the time has passed.

fetchText

fetchText : {e : HFunctor} -> {{ev : dom <: e}} -> String -> Co e String

A URL’s text, fetched (a GET); where that fails, what the browser says of it.

textIn

textIn : {e : HFunctor}
       -> {s : Type}
       -> {{ev : dom <: e}}
       -> With s Document
       -> Element
       -> String
       -> String
       -> Co e Element

An element with some text in it, put in a parent.