1 Description

Document templates, and web page templates in particular, are rather useful in everyday tasks, yet document template engines tend to be underpowered – that is, generally they don't provide much more than "include" directives and variables substitution, excluding those that provide things like cycles and variables, which is beyond template tasks (i.e., not even declarative).

But what if we'll build templates on top of inductively defined data types, turning those templates into type definitions, and into basic definitions of their "Show" instances at once? Things like polymorphism would come naturally, general editing facilities could be added as well, while expressiveness would be rather good.

"Delays" could be added to allow things like navigation (and to avoid rendering everything in a single document, especially in case of web pages), and functions could be added easily, in place of data constructors on update (making it reactive at once, perhaps), though it'd be a bit beyond of the original idea.

The described approach is quite generic, but the idea came in context of making a web site, so keeping web UI, together with some subjective web site preferences in mind.

2 On implementation

2.1 DONE Basic language

Dependently typed lambda calculus is both expressive and simple, so taking it as a base. I've mostly copypasted Simpler, Easier! implementation for that, and there's a nice description of it.

2.2 DONE Extending with data types

There's no need to add new constructors into AST, though it might be useful later; type and data constructors could be added just as axioms, but with a few checks to avoid breaking things. Some related materials are collected on the "links" page, in "GADTs, (Co)inductive types, CciC" section. Oh, and there's no need in codata for templates (at least I'm failing to see application of it; some requests or interaction, perhaps?).

2.3 DONE Extending with templates

A simple way would be to attach chunks of templates into Pi type, providing one for every constructor. Another way would be to add an axiom "Template: Type → String → Type", but while it's possible to describe a lot of things in such a language, it's not particularly handy to work with it. And one more template chunk should go to Env, in that case, because it's required to define n+1 template parts for n constructors. Does not look particularly nice, but it's mostly a matter of program architecture and doesn't matter much.

2.4 DONE Extending with delays

Tried a couple of options, and the following approach seems nicer: a usual type of natural numbers, LNat, which is used to index other types, and a function "pred". Once a zero of that type appears in a constructor argument's type, it's time to stop rendering. Works nice with implicits, and here's an example of such a type in Idris:

data LazyList : Type -> LNat -> Type where
  Nil : {a: Type} -> {n: LNat} -> LazyList a n
  Cons : {a: Type} -> {n: LNat} -> a -> LazyList a (pred n) -> LazyList a n

Later, in order to implement navigation (including, say, pagination), in case of web pages, links should be inserted in place of hidden values, referencing ID of the argument that provided the initial (constant) number, so there will be enough information to increase it by the initial value, and then skip rendering of values indexed by numbers that are higher than the initial. Though it would require changing the types, and perhaps type-checking everything again, which is not nice.

Another option is to load by one record in case if that value is zero on the first iteration.

2.5 DONE Extending with implicits

When it'll come to editing, it won't be nice to provide things like types for polymorphic types' constructors on every application, so implicits are required (edit: and they are used for delays now).

Have not found much descriptions by now; Idris uses tactics to eliminate them, Agda uses metavariables, and I was looking for an easier way for now. Coq documentation lists different types of implicits, which was rather helpful; so, at least contextual implicit arguments should be used, though it'd be nice to extend with other kinds later.

2.6 DONE Extending with primitive types

That's pretty simple: just one more AST constructor, carrying required types, axioms for those types, and a function that provides those types' names, to be used from a type checking function. Or a type class could be used to map types defined in underlying language, or something like that.

2.7 Updating values

There's (at least) two options:

2.7.1 Language

That is, a bit of parsing, and raw edit. There's not much to write here.

2.7.2 UI

This is going to be about web pages, though nothing prevents from using a similar approach in other cases.

Everything should be rendered in the same way as for regular view, but primitive types should be editable via type-specific mechanisms (textareas, [custom] inputs), and buttons should be appended to every value (perhaps appear on hover only, but be there), one button for each constructor of a required type in that position. And for each function that is capable of returning that type, in case if there will be functions.

For list-like structures, a special kind of update should be added, that would help to insert and delete elements in the obvious way: in case of lists, just add an element on Cons instead of constructing a new list, and provide a function to remove single elements from a list; they could be defined using additional syntax, marking related constructors' arguments.

In order to avoid non-necessary typechecks of the whole value (e.g., site content), only changed value's type should be checked first: there's no need to check the rest if it's the same, and it should be relatively easy to implement such local checks.

Relatively fat client would be nice here, but fat JS clients, while teamed up with browsers with lots of other things opened, tend to be laggy, and often even glitchy, so it'd be better to have a light JS-free version as well.

2.8 Templates language

Have not put much thought into it, but something like this should work for HTML templates: file name (or a record in database, or something like that; that is, it could be external, and in some cases it would make sense to make it external) for type name, first line for type constructor's arguments, and then, say, curly brackets for definitions: inside comments for constructor names, and outside – for their arguments. Curly brackets for implicits (inside those other brackets, making them double), square brackets to mark arguments for those special updates described above. Would look like this, for a basic blog:


Type LNat
<!-- {Nil} -->
{{a: Type}}
{{n: LNat}}
{List a n}
<!-- {Cons} -->
{{a: Type}}
{{n: LNat}}
{x: a}
{[List a (pred n)]}
{List a n}


<!-- {MkPost} -->
<div class="post">
  <!-- String is a primitive type, and this is a basic comment -->
  <div class="title">
  <div class="content">


<!-- {MkBlog} -->
<div id="blog">
  {List Post 10}

2.9 TODO Mapping AST to a map

Or to a database, with access by ID. And optimizing it for navigation, perhaps; otherwise bigger sites could be much slower.

2.10 TODO Extending with access control

Need to think more about it.

3 Code

Pushing the code into this github repository, so it can be found there.