In this tutorial I am going to explain the core functionality provided by this library and shed some light on implementation details, design decisions, and the module structure of idris2-dom. This whole thing is still evolving - as is Idris2 itself - so expect stuff to change frequently until things settle down a bit.
Most of the several thousands of lines of codes in this library have
been automatically generated by the
idris2-webidl
program from a set of Web IDL
specifications, collected from several resources on the
internet. You can find the specs used in the idl folder
of the idris2-webidl project.
The generated code consists of a set of external type
declarations (to be found in the submoduls of
Web.Internal whose names end on Type.idr). This was done to
avoid cyclic module dependencies, since many of these types
are freely shared across specifications and the related
modules. The whole set of external types is reexported
by Web.Internal.Types, which also includes the subtyping
relations (more on that later).
FFI bindings are defined in submodules of Web.Internal ending on Prim.idr.
If you are interested in how to interact with JavaScript through the FFI,
you will find many examples there.
The actual API of this library is provided by the
modules in Web.Raw, which provide a convenience layer around
the FFI primitives.
Finally, direct submodules of Web add yet another layer of
safety and convenience. Unlike the modules in Web.Internal and Web.Raw,
these are hand-written and still lacking a lot of functionality.
All of the above rely on a set of utility functions and types provided
by the submodules in folder src/JS and reexported by module JS
itself. This includes interfaces for converting values from and to
their FFI representation, utilities for subtyping and safe casts, nullable
and undefined values, plus a set of integral types, which are represented
by JavaScript Numbers in the backend, unlike the Idris2 integer primitives,
which all are bound to BigInt (although this might change in the
future).
It is the goal of this tutorial to explain how all these pieces fit together.
Below is the logic of a simple web page consisting of a button and a text field. Users can enter their name in the text field and receive a friendly greeting upon clicking the button. At the same time, during text input, the program checks whether the name entered is a palindrome or not.
module Tutorial
import Data.String
import JS
import Web.Dom
import Web.Html
import Web.Raw.UIEvents
checkPalindrome : String -> String
checkPalindrome s =
let s' = toLower s
in if s' == reverse s'
then "Cool! Your name is a palindrome."
else "Your name is rather mundane..."
export
prog : JSIO ()
prog = do
btn <- createElement Button
textContent btn .= "Click me!"
Element.id btn .= "the_button"
txt <- newElement Input [ HTMLInputElement.type =. "text"
, placeholder =. "Enter your name here."
]
txtDiv <- createElement Div
lenDiv <- createElement Div
outDiv <- createElement Div
onclick btn ?> do name <- txt `get` value
textContent outDiv .= #"Hello \#{name}!"#
oninput txt ?> do reply <- checkPalindrome `over` value txt
textContent lenDiv .= reply
ignore $
(!body `appendChild` btn) *>
(!body `appendChild` txtDiv) *>
(!body `appendChild` outDiv) *>
(!body `appendChild` lenDiv) *>
(txtDiv `appendChild` txt)You can give this a try in the browser by replacing the
main function in Main with main = runJS Tutorial.prog
followed by building the doc package: idris2 --build doc.ipkg.
Now, load the doc.html file in the project's root folder in your browser.
It will not look very nice, but it should behave as described.
The program is of type JSIO (), which is just an alias for
EitherT JSErr IO (). Since the world of JavaScript is highly unsafe,
error handling comes built-in in the default IO monad we use (however, we do
not catch a lot of errors so far).
The error type JSErr is defined in module JS.Util and reexported
by module JS, which provides the core types and functionality
required for interacting with the world of JavaScript.
In order to run a program of type JSIO (), we need a way to
deal with the possibility of errors. The most basic option
is function runJS, which logs any error to the console
(function JS.Util.consoleLog). MonadError exported by
Control.Monad.Either in base provides additional functionality
for error handling.
Function Web.Dom.createElement takes a tag from an enum type
and returns a properly typed, newly created HTML element.
This is a convenient wrapper around the automatically generated
Web.Raw.Dom.Document.createElement. In addition,
Web.Dom.newElement takes an additional list of modifiers
for adjusting the newly created element. This is especially
useful for setting an element's attributes (see also the section
about Attributes below).
This is probably the right place to explain how safe type casts
are handled in this library. There are mainly two ways to inspect
the type of a value at runtime in JavaScript: One is function
typeof, a binding to which is available in JS.Util. This
function is mostly useful to figure out the types of primitives
like numbers and strings. For other types like HTMLElement, which
also inherits methods and attributes from Node and Object
(and some others), it is necessary to inspect
the chain of prototype objects to figure out, from which
types a value inherits its functionality.
External types, whose type can be verified at runtime by one of
the two means described above, implement interface
SafeCast from module JS.Inheritance. This module also provides
the two main (unsafe) functions to inspect and change a value's type at runtime
plus some utility functions.
Please note, that SafeCast is meant to be used for external types only.
Note also, that SafeCast is typically not the thing you want
for upcasting (that is, casting a type to one of its parent
types or included mixins): For this, there is another interface,
which will be desribed below.
As an example: In the program above, we know that the element
with ID "the_button" is a HTMLButtonElement. However,
function getElementById from Web.Raw.Dom returns a Maybe Element.
If we'd like to disable this button, we first have to cast it to
the proper type. We can use safeCast for this:
export
disableBtn : JSIO ()
disableBtn = do
maybeElem <- getElementById !document "the_button"
let maybeBtn = maybeElem >>= castTo HTMLButtonElement
for_ maybeBtn $ \btn => do
disabled btn .= True
consoleLog "Disabled button"You can try the action above by modifying our original program:
namespace Alt
main = runJS $ prog *> disableBtnSince looking up an element and refining its type by downcasting
is a common pattern, there are functions castElementById
and htmlElementById in Web.Dom:
export
disableBtn2 : JSIO ()
disableBtn2 = do
maybeBtn <- htmlElementById Button "the_button"
for_ maybeBtn $ disabled =. TrueAttributes are amongst the most common members of Web IDL definitions.
In this section, we are talking about non-static read/write attributes.
Readonly attributes are mapped to plain functions in this library.
Read/write attributes, however, are represented by an indexed
data type and come with quite a few utility functions and operators.
All of this is provided by module JS.Attribute. Lets have a look
at how all of this works under the hood.
All flavors of JS.Attribute.Attribute consist of a
getter (of type JSIO $ f a for a context f and return type a)
and a setter (of type f a -> JSIO ()). They differ in the context,
in which a value is wrapped (I if the attribute is mandatory
and non-nullable, Maybe if it is mandatory but possibly null,
and Optional, if the attribute might be missing altogether, in
which case the getter at the FFI returns undefined), as well as
whether it is possible to always get a concrete value when invoking
the getter (this is even possible for optional attributes, if
they have a default value defined in the specification).
Although the JavaScript constants null and undefined both describe
a missing value, they can - depending on context - still have different
semantics, therefore we use two different pairs of Idris2 types to deal with
them. In foreign function calls, nullable values are represented
by external type Nullable a from JS.Nullable, which is converted to Maybe a
in the *Raw modules. Optional attributes and function arguments
are represented by the external type UndefOr a at the FFI and
marshalled from and to Optional a, a monadic type isomorphic to
Maybe a. UndefOr and Optional are both defined in JS.Undefined.
The JS.Attribute modules provides some utility functions and operators
for accessing and updating the value stored in an attribute.
New operators are always a delicate topic, so this module only adds six
of them. (.=) is an infix version of set, as is (=.), which
is useful when the object, to which an attribute belongs, is stored
in a traversable structure. Likewise, (%=) modifies an attribute's
stored value, and (=%) is again the flipped variant.
Finally, there are two operators (!>) and (?>) use for registering
callback functions, a topic discussed in more detail below.
Idris values can typically not be used directly in FFI calls.
To marshall between the worlds of raw JavaScript and Idris, two
interfaces are provided by JS.Marshall: ToFFI and FromFFI.
Both interfaces take two type parameters, the first being an
Idris type, the second its external representation. As
an example, consider the following Answer data type:
data Answer = Yes | NoValues of type Answer should be represented by JavaScript booleans,
for which there already is an external type: JS.Boolean.Boolean, which
also provides values for the JavaScript constants true and false.
It is therefore straight forward to implement ToFFI for Answer:
ToFFI Answer Boolean where
toFFI Yes = true
toFFI No = falseNote, that conversions to the FFI should always succeed as types in Idris are considered to be more precise than the ones used in the backend.
Coming from the backend is only slightly more involved. First, the
conversion might fail (this shouldn't happen if functions implemented
in JavaScript adhere to their spec, but one can never know for sure),
so we return a Maybe. In addition, we have to compare the FFI value
against the external constants. For this, heterogeneous equality
function JS.Util.eqv can be used,
which invokes the JavaScript === operator internally. Here's the
implementation of FromFFI:
FromFFI Answer Boolean where
fromFFI v =
if eqv v true then Just Yes
else if eqv v false then Just No
else NothingMost of the time, foreign function calls wrap their result in PrimIO.
Values wrapped this way can be converted to their Idris representation
by means of JS.Marshall.tryJS. This function takes an additional
String, which will be used to specify the call site in the
error in case the conversion fails:
%foreign "javascript:lambda:x => { console.log(x); return x > 0; }"
prim__logAndTest : Double -> PrimIO Boolean
logAndTest : Double -> JSIO Answer
logAndTest d = tryJS "Tutorial.logAndTest" $ prim__logAndTest dFor some types it is harder to write generic conversion
functions. This is especially the case for callbacks, which
are for instance used as event listeners in browser elements.
Like most Web IDL definitions, callbacks get their own external
type (see for instance Web.Internal.DomTypes.EventListener).
However, it is not possible to directly write a ToFFI implementation
for the corresponding Idris function for two reasons: First, interface
resolution does not work for function types (but see below), and
second, converting an Idris function to a callback is not referentially
transparent, since each conversion will create a new JavaScript
function object.
Therefore, we need a new interface for handling this corner case:
JS.Callback.Callback. Automatically generating instances of this
interface with proper marshalling proved to be hard,
and since there are not many callbacks
defined in the specs, I chose to implement these manually.
Note, how interface resolution for Callback is based on the
external type, so it is no problem that the second type is an
Idris function.
Attributes come with two utility operators for registering
callbacks: (!>) allows us to register a unary callback function
while (?>) registers an action which ignores the value passed to it.
The following code snippets provides examples for both use cases:
complainOnClick : HTMLButtonElement -> JSIO ()
complainOnClick btn = onclick btn ?> consoleLog "Don't touch me!"
doComplain : MouseEvent -> JSIO ()
doComplain me = do
shiftPressed <- shiftKey me
if shiftPressed
then consoleLog "DON'T TOUCH ME!"
else consoleLog "Don't touch me!"
export
complainSomeMore : HTMLButtonElement -> JSIO ()
complainSomeMore btn = onclick btn !> doComplainThis completes our analysis of the functions and techniques used in the initial program. Some additional topics are discussed in arbitrary order below.
Generated JavaScript files can be further compressed and optimized
by using a recent release of the Closure Compiler.
It needs to be recent enough to support BigInt literals, which is
available through the ECMASCRIPT_2020 output option.
Here is an example closure.sh shell script that can be used to
shrink Idris2-generated .js files:
#!/usr/bin/env bash
java -jar ~/downloads/closure-compiler-v20210406.jar \
--language_in ECMASCRIPT_2020 \
--language_out ECMASCRIPT_2020 \
--jscomp_off undefinedVars \
--js $1
This script can then be invoked with
closure.sh build/exec/runTest.js > test.jsIn my experience, this leads to a reduction in size of about 30% and a speedup of about 100% (compiled .js files run about twice as fast).
As explained at the beginning of this tutorials, the DOM bindings in this library have been generated automatically based on Web IDL specifications. It therefore makes sense to have a look the different kinds of toplevel definitions specified in Web IDL.
These describe function types: An identifier (the callback's name), a return type plus a list of typed arguments. In addition, callback interfaces can specify an arbitrary number of constants, which are mapped directly to corresponding nullary function declarations in Idris.
As discussed above, callbacks and callback interfaces get their
own external type of the same name as in the specifications
plus some function for marshalling an appropriately typed
Idris function to this external type. In addition, for
some callback function types it makes sense to manually
implement interface Callback. This hasn't been done for
all specified callbacks so far.
Since the type of a callback cannot be inspected at runtime, registered callbacks will not be converted back to Idris functions when returned by an API function.
Example: Web.Internal.DomTypes.EventListener.
A Web IDL dictionary defines a JavaScript object with an
associated set of read / write attributes. A dictionary's type cannot
easily be inspected at runtime, therefore they come without
implementations of SafeCast.
Dictionary attributes can be mandatory or optional, which is
reflected by the type of generated Idris Attributes as described in
the section about attributes above.
Dictionaries can have a weak form of subtyping relation: If a JavaScript object has attributes of the same names and types as the ones listed in a Web IDL dictionary definition, this object can be as an argument to functions expecting such a dictionary value. This subtyping relation is given in the Web IDL specifications for the dictionaries mentioned there, and corresponding subtyping relations are generated for and provided by this library (see below for an explanation, how subtyping is handled in this library).
For every dictionary, there are one or two constructors named new
and new' available. Constructor new' is only available, if
the dictionary has optional attributes, which are then missing
from this constructor's argument list. Constructor new, on
the other hand, can be used to
set all attributes (optional and required ones) explicitly.
Example: Web.Internal.DomTypes.EventInit.
In Web IDL, an enum corresponds to a set of string constants.
While in the JavaScript backend these are just ordinary string values
(but out the specified set of allowed values), our code generator
generates proper Idris enum types for them, together with corresponding
functionality for converting these values from and to String.
Example: Web.Internal.DomTypes.ShadowRootMode.
See Mixins below.
A Web IDL interface defines a proper type together with associated
attributes and operations, for which it is possible
to verify at runtime, whether a value is of this type by inspecting
its prototype object chain. The Idris2 external types corresponding
to interfaces therefore come with a SafeCast instance.
Interfaces specify subtyping relations (each interface can have at most one parent type), and these relations can be used for upcasting values in Idris to one of their parent types.
Example: Web.Internal.DomTypes.Element.
A Web IDL mixin defines a set of attributes and operations shared
between different interfaces without them being related by subtyping.
It is typically not possible to directly check at runtime, whether a value
belongs to a given mixin, therefore the corresponding external Idris
types come without implementations of SafeCast. It is, however,
possible, to cast a value to a mixin type by going via one of the
interface types implementing that mixin.
The Web IDL specifications use includes statems to specify, which interfaces include the functionality of a given mixin.
Example: Web.Internal.HtmlTypes.GlobalEventHandlers.
A Web IDL namespace defines a singleton object with associated
attributes and operations. Namespaces are not yet covered by the
code generator, but there is only one namespace defined in
the whole spec used so far: CSS, with a single function for
escaping CSSOMStrings.
Type definitions define type aliases. These are not present in this library: The code generator resolves all type aliases before converting them to Idris types. While this renders some types drastically more verbose, it makes inspecting the type of an unfamiliar function much easier.
Subtyping relations as described for interfaces, mixins, and dictionaries,
are handled by interface JS.Inheritance.JSType. Implementations of
this interface list associated parent types and mixins for an
external Idris type. Function up and operator (:>) can be
used to safely upcast a value to one of its parent types or
implemented mixins.
Including the functionality for automatically upcasting
arguments in API functions is a double-edged sword. On the one hand,
it allows us to call these functions without having to manually
invoking up on every single occasion, on the other hand
it prevents Idris to figure out which function we mean in case
of overloaded function names. Therefore, automatic argument
upcasting is only present for types corresponding to known parent interfaces
(that is, interfaces inherited by at least one other type in the
spec) as well as all dictionaries and mixins.
For interfaces at the leaves of the inheritance tree, it makes no sense to worsen type inference as we will hardly ever need the additional gain in flexibility.
Two examples: Web.Dom.Node.firstChild abstracts over the
parent node's type, while Web.Html.HTMLButtonElement.checkValidity
uses concrete types, since there are no child interfaces for
HTMLButtonElement in the spec.
To be added...
The object type is at the root of the inheritance tree in JavaScript.
Almost every value that is not a primitive inherits from object.
Module JS.Object provides external type Object for representing
external objects.
However, this is by far not the most interesting part about objects
in JavaScript. Objects are efficient mutable mappings from Strings to
arbitrary values, and module JS.Object gives users access to this
functionality by means of a mutable linear-access object type LinObject
and an immutable variant IObject, that can only be used for looking
up values. In addition, there is an abstract Value data type together
with functionality for encoding Idris2 values from and to JSON by
means of external functions JSON.stringify and JSON.parse.
Note, that unlike most other external types, Object comes without an
instance of SafeCast. Such an instance would allow us to "unfreeze"
an immutable IObject, allowing us to mutate this object, thus
breaking referential transparency.
The Web IDL allows the definition of functions with a variable
number of arguments. In this library, we support such functions
by allowing them a List argument instead of a variadic number
of arguments. When passed to the FFI, the list is converted to
a IO $ Array a (see Lists ToFFI implementation in JS.Array).
In our example program, we could therefore also have added the different nodes to the body like so:
addNodes : HTMLButtonElement -> HTMLDivElement -> HTMLDivElement -> JSIO ()
addNodes btn txtDiv outDiv =
ignore $
(!body `append`
[ Here $ btn :> Node
, Here $ txtDiv :> Node
, Here $ outDiv :> Node
])In this case, we wouldn't have gained much, as we'd need to manually upcast the different elements and inject them into the required sum, but for other functions with less complex argument types this can be sometimes quite convenient.
To be added...