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 |
|
|
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 —
illuminateis defined as an interface -
Types — The types that illumination describes