Pantagruel
- This article is not detailed enough and needs to be expanded. Please help us by adding some more information.
| Designed by | Z. D. Smith |
|---|---|
| Appeared in | 2021 |
| Type system | static, strong, explicit |
| Computational class | Quadratic |
| Reference implementation | [1] |
| File extension(s) | .pant |
Pantagruel is a specification language for specifications. A Pantagruel document specifies the vocabulary and structure of a system without detailing its semantics. Instead of execution, the reference implementation of Pantagruel checks that a document is well-formed and well-typed.
Pantagruel constrains the human thinker into some of the syntactic forms of first-order logic and computer programming. In doing so it is hoped that the thinker will encounter elements of their thought which require further precision. ~ Z. D. Smith
Example
The following example specifies the wikipedia:haiku poetic form.
module HAIKU. Poem = [Line]. Line = String. scans? p:Poem => Bool. // A haiku is a poem of exactly three lines. scans? p -> #p = 3. // Each line has a prescribed number of morae; the numbers of morae go 5, 7, 5. scans? p -> morae (p 1) = 5 and morae (p 2) = 7 and morae (p 3) = 5. where // A mora is like a syllable, but shorter; it is known in Japanese as 音. // To evaluate a line we count its morae. morae l: Line => Nat.
Complexity Class
Types can be used before definition, allowing a linear number of type constraints to pile up prior to resolution. As such, even a linear-time type-checker can be forced to spend quadratic time reinterpreting each prior chapter's partially-resolved types in terms of the next chapter's not-yet-specified types, taking quadratic time in total. However, this is only a theoretical weakness at present.