Illumination

Illumination provides human-readable display strings for types. Where valid constrains what values are allowed (returning Boolean), illuminate describes how values are shown (returning Text).

Product Illumination

For product types, an illuminate block is a single expression that produces Text:

type Pet
  name: Text
  age: Integer
  species: Species

illuminate Pet
  name ++ " " ++ age as Text

Fields are referenced directly by name inside the illuminate body. The entire expression must produce a Text value.

type User
  first: Text
  last: Text

illuminate User
  first ++ " " ++ last

Union Illumination

For union types, provide case patterns for each tag:

union Color
  red: Integer
  blue
  green: Text

illuminate Color
  red: intensity. "Red(" ++ (intensity as Text) ++ ")"
  blue: "Blue"
  green: shade. "Green: " ++ shade

Tags with payloads bind a variable. Nullary tags provide a literal string. A wildcard _ can serve as a default:

union Response
  success: Text
  error: Text
  pending

illuminate Response
  success: msg. "OK: " ++ msg
  _: "Non-success response"

Recursive Illumination

Call illuminate on nested fields to compose display strings:

type Bar
  zippy: Text

illuminate Bar
  "||" ++ zippy ++ "||"

type Foo
  name: Text
  bar: Bar

illuminate Foo
  name ++ (illuminate bar)

The expression illuminate bar calls the illumination of the nested Bar field, producing its display string inline.

This also works across product/union boundaries:

type Result
  color: Color
  response: Response

illuminate Result
  "Color=" ++ (illuminate color) ++ ", Response=" ++ (illuminate response)

Optional Default

Use ? to provide a fallback for optional fields:

type Profile
  name: Text
  nickname: Text?

illuminate Profile
  nickname? name

If nickname is present, it is used; otherwise, name is the fallback.

How Illumination Differs from Validation

valid illuminate

Return type

Boolean

Text

Purpose

Constrain what values are allowed

Describe how values display

Multiple expressions

Combined with &&

Combined with ++

SMT verification

Yes

No

Both valid and illuminate are interfaces. Their combiner functions differ: valid combines with && (all must hold), while illuminate combines with ++ (concatenation).

Using Illumination in Code

Call illuminate as a regular function anywhere you need a display string:

watFoo: f:Foo. Text
  "wat: " ++ f.name ++ (illuminate f)

See Also

  • Validation — The constraint counterpart to illumination

  • Interfaces — illuminate is defined as an interface

  • Types — The types that illumination describes