Types

Types exist to ensure that apps are treating data properly.

Formal definition

A node’s type can be one of the following:

$\tau :\equiv$

• $c$ (constant)
• $\alpha$ (type variable)
• $\mu \alpha . \tau$ (inductive type)
• $( \ell_k : \tau_k )_k$ (record type)
• $\{ \ell_k : \tau_k \}_k$ (sum type)
• $\#n$ (singleton type)

Constants may be node references, unit, unsigned/signed integers, decimal, strings, booleans, instant (or timezone-aware timestamp), or URL

It is possible in the future that node references are also made using URLs, but the URL format will need to be decided upon by then.

Notes

• All nodes must belong to closed types. This means type variables cannot exist at the top-level.
• When shown in the panorama UI, the constant type will not be shown as a separate type. Instead the actual type itself will be inlined.
• The type registry doesn’t canonically exist in the database (it may exist in the form of system logs). Instead, apps register their types on boot. Everything is known to the panorama daemon after app initialization.
• The following constant types have their fields embedded directly into the node table:
  • Number (integer, bigdecimal), string, boolean: value
  • Sum: label (which variant is used?)
• Record types are essentially a collection of forced attributes. A node with a record type must contain every field listed in the labels of the record type.
• The panorama type system is structurally typed. #TODO Maybe add some convenient way of introducing ways to distinguish types apart?

Convenient types

• $\textsf{Optional}(\tau) :\equiv \{ \texttt{'none} : () , \texttt{'some} : \tau \}$
  The optional type.

What is the point of a singleton type?

Singleton types only consist of a node ID. The point of this is so apps can create types that are forced to have exactly a single node.

Note

Apps with dashboards (mail) may create a type that represents the “entrypoint” into their application. The process of creating it would look like this:

• Upon app registration, I declare that I want a singleton type to be registered as panorama-mail/entry.
• A node id will be assigned, if it doesn’t already exist.
• The application is returned the node ID.
• The application can then register links to that node ID, and it can register a handler.

When an app is registered, its types are parsed and registered into the database. At the time of writing, if the node ID it refers to has already been found in the database, the type of the node will be checked against the given type. If it doesn’t match #TODO

Attributes

Nodes contain attributes. An attribute is a link to another node. Attributes are typed, and the node it’s linked to must have that type.