Language Walk Through
In the beginning, Truth is formless and empty. There exists absolutely nothing–no strings, no numbers, no built-in framework. It is up to you to define the truths that exist in your domain. In order to add something to your domain, just write it out:
Employee
We've now just added the type Employee to our domain. Still following along? :) (it will pick up soon)
The atomic unit in Truth is the Statement. A statement takes the following form:
[Has a] : [Is a]
Both sides of a statement are optional. This is why a file containing only the text Employee is a valid statement: It establishes that our domain has an Employee. We can use the colon syntax to build upon this and establish an is a relation:
Developer : Employee
Which would be read in English something like: A Developer is an Employee.
Establishing a has-a relation occurs with another statement nested inside, expressed via indentation. Here's the full file so far:
Employee
Developer : Employee
Manager : Employee
In English, this roughly translates to: Employee is a known type. A Developer is an Employee. A Developer has a Manager, who is also an Employee.
The only other operator is the ellipsis (...) operator. Appending it to a type causes the type to be a plural:
Employee
Developer : Employee
Manager : Employee
Subordinates : Employee...
The last line translates to A Developer has Subordinates, who are all Employees.
And that is basically the entire language. Everything else is just the application of the logic that naturally come about when declaring relations.
As stated, Truth starts from a completely void state. So lets define the basic tenets of a programming language, starting with booleans:
Type
Boolean : Type
And now lets define what a boolean is:
true : Boolean
false : Boolean
Let's add some of the other basics
String : Type
Number : Type
Class : Type
Going beyond the basics, let's define some more specialized types:
Email : String
Currency : Number
Truth supports regular expression literals using the familiar /regex/ syntax from JavaScript, Perl, and others. Regular Expressions match on the is-a side of a statement. This feature can be used to define your own well-typed language literals:
/".*?"/ : String
/[\w-\.]+@([\w-]+\.)+[\w-]{2,4}/ : Email
/[0-9]+/ : Number
/\$[0-9]{1,}(\.[0-9]{2})?/ : Currency
Putting it all together:
Type
Boolean : Type
String : Type
Email : String
Number : Type
Currency : Number
Class : Type
true : Boolean
false : Boolean
/".*?"/ : String
/[\w-\.]+@([\w-]+\.)+[\w-]{2,4}/ : Email
/[0-9]+/ : Number
/\$[0-9]{1,}(\.[0-9]{2})?/ : Currency
Employee : Class
Name : String
WorkEmail : Email
CompletedTraining : Boolean
Salary : Currency
Paul : Employee
Name : "Paul"
WorkEmail : paul@company.com
Salary : $50000.00
CompletedTraining : true
This works because the compiler knows that anything matching the specified regular expressions, is a X. So $50000.00 is a Currency. If the salary was set to true, an error would be generated.
You can define your own language literals for anything you can validate with a regular expression: complex numbers, license plate numbers, postal codes, etc.
In order to act as an adequate replacement for JSON, there must be a way to declare the existence of a Type, without having to assign it an explicit name. And so the left side (which we call the has-a side) of a statement is optional. When the has-a side of a statement is omitted, it creates what we call an Anonymous Type. Building upon the employee example from above, if we were to store all the employees in a file, you wouldn't want to name every single employee record. And so a file may look like this:
: Employee
Name : "Paul"
WorkEmail : paul@company.com
Salary : $50000.00
CompletedTraining : true
: Employee
Name : "Kim"
WorkEmail : kim@company.com
Salary : $50000.00
CompletedTraining : true
Although Truth is stateless, the order of declarations is still relevant (like CSS). Truth therefore supports a syntax reminiscent of order-based function parameters as is present in most programming languages. And so the above could be further shortened to:
: Employee
: "Paul"
: paul@company.com
: $50000.00
: true
: Employee
: "Kim"
: kim@company.com
: $50000.00
: true
Because Anonymous Types don't have a name, other types have no way to inherit from them. Therefore, in practice they're used to store what would be the "data" of your file.
In many cases, Truth can also perform type inference. If the right side of a statement (which we called is-a side) is omitted, the following type inference rules are applied:
If the type is being overridden from a super type, it's assigned the type as defined by the super type. For example:
SuperClass : Class
Field : String
SubClass : SuperClass
// The type is inferred as String.
Field
In the case where nothing is being overridden, the compiler works it's way up the scope chain to find a matching type:
Class : Type
Field : Type
// The type is inferred as Email.
Email
When the is-a side of a statement is omitted, and the above type inference strategy fails, the statement creates in what we call a Fresh Type. Fresh types do not gain anything from any ancestor. The top-most statement in a Truth file is usually a fresh type.
// Type is fresh
Type
String : Type
You can force a fresh type by making it equal to itself:
// First Foo
Foo
Bar
// Second Foo, not a sub type of the first Foo,
// because it was essentially re-declared.
Foo : Foo
It should be obvious from the above examples that Truth follows the basic logical premise that if A is a B, and B has a C, then A must have a C. And so Truth has an implicit notion of inheritance. Furthermore, the syntactical nature of Truth lends itself very well to expressing type unions (or multiple inheritance). Simply declare a particular type to be of an additional type with a comma, and a type union is implicitly formed:
Material
BoltMaterial : Material
ScrewMaterial : Material
Steel : BoltMaterial, ScrewMaterial
Copper : ScrewMaterial
Commas are the English-equivalent of the word "and". They can used on both the has-a, and is-a side of a statement. This allows you to encode your statements in a syntax loosely reminiscent of CSS selectors. For example the above could be rewritten as:
Material
// BoltMaterial and ScrewMaterial are a Material
BoltMaterial, ScrewMaterial : Material
// Steel is a BoltMaterial and a ScrewMaterial
Steel : BoltMaterial, ScrewMaterial
Copper : ScrewMaterial
This creates a type hierarchy that looks like the following:
The instantiation of a type can be fragmented across multiple statements. When this happens, the compiler merges these Type Fragments into a larger type, which we call a Fragmented Type. You can think of this feature as similar to partial classes from C# or declaration merging from TypeScript, but with a unique set of rules.
String
Required
// Given the following:
Customer
Name : String
// The below:
Customer
Name : Required
// Is functionally equivalent to this:
Customer
Name : String, Required
There may be a valid cause of concern that this could lead to unexpected side effects. Consider the following example:
String
Email
User
ID : Email
//
// Thousands of lines of Truth,
// most of which was written by other people
//
User
// ID is actually now and Email and a Number,
// which doesn't make much sense
ID : Number
We plan to solve this problem through plugins to the editing software that displays visual cues when fragmented types are in use.
Fragmented types also have a characteristic that we call coercive down-typing. When two fragments declare the same type, but one is a subtype of the other, the type that results are a union of the most derived types in the set. Consider the follow example:
Number
Decimal : Number
Currency : Decimal
Product
Price : Number
Product
Price : Decimal
Product
Price : Currency
Here, Price has the type of Currency, because when Number, Decimal, and Currency are put together, Currency is the most derived type, and so it becomes the actual type of Price. This also works across unions:
Number
Decimal : Number
Currency : Decimal
Required
Constant
Product
Price : Number, Constant
Product
Price : Decimal, Required
Product
Price : Currency
// Results in:
Product
Price : Currency, Constant, Required
Truth enforces covariant subtyping rules on all types that extend from others. If a child inherits from a parent, it's OK to re-declare any entities that the child gains via the inheritance. However, the re-declared type must remain as a subtype of parent's declaration. For example, the following is an error:
Seat
LeatherSeat : Seat
SparkPlug
Car
Seats : Seat...
LuxuryCar : Car
// Error, SparkPlug is not a Seat
Seats : SparkPlug...
Conversely, the following is valid:
Seat
LeatherSeat : Seat
SparkPlug
Car
Seats : Seat...
LuxuryCar : Car
Seats : LeatherSeat...
Also interesting is how this plays out when combined with unions:
String
Email : String
Required
Record
Value : String
MyRecord : Record
// No problem
Value : String, Required
Astute readers will have inferred the recursive nature of statements, and therefore, their ability to be nested within each other. For example:
Type
Number : Type
/[0-9]+/ : Number
String : Type
MinimumLength : Number
MaximumLength : Number
Foo : Type
Value : String
MinimumLength : 5
MaximumLength : 10
Essentially, when an entity is declared to be of a certain type, it gains the entities that the referenced type has been declared to have. The types of these gained entities can then be re-declared, in accordance with the rules around covariance.
Of course this doesn't actually enforce minimum and maximum length, but it does provide meta-data necessary for an external tool to do so.
Truth supports the idea of dependent types. The type of an entity can be declared as a subtype of a sibling. For example:
Type
Equation : Type
Left : Type
Right : Left
The above means: Left is a Type, but Right has to be type-compatible with whatever Left is. Showing this a little more concretely:
Type
Cow : Type
String : Type
Email : String
Equation : Type
Left : Type
Right : Left
StringEquation : Equation
Left : String
// Works. String would work too. But not Type, and definitely not Cow.
Right : Email
Types can also be inter-dependent:
Type
Equation : Type
Left : Right
Right : Left
Which essentially means that Left and Right are essentially fresh types, but they both need to be subtypes of each other (which is another way of saying that they must be exactly the same).
Building upon Fragmented Types, it's possible to re-declare a sibling to apply additional restrictions. The resultant type is folded:
Type
Expression : Type
Equation : Type
Left : Expression
Left : Right
Right : Left
The above is essentially equivalent to the previous example, but with the added restriction that Left and Right both need to be subtypes of Expression.
By default, types are said to be singular. However, a type can be said to be a plural of a type by appending the ellipsis (...) operator:
// Number is a singular fresh type
Number
// Numbers is a plural of numbers.
Numbers : Number...
The concept of a plural roughly translates to the idea of an array found in most programming languages. Types that are defined as plural can any number of nested types (as is the case with any type). However, any type nested inside a plural must be compatible with the plural. Below are some examples to illustrate this point.
Let's begin with a simple definition of some animals, with a base type:
Animal
Rabbit : Animal
Dog : Animal
Cat : Animal
The following code would be valid. The types owned by Animals are anonymous types, which are all compatible with the base type Animal:
Animals : Animal...
: Rabbit
: Dog
However, the following would be invalid, because String is not an subtype of Animal:
Animal
Rabbit, Dog : Animal
String
Animals : Animal...
: Rabbit
: Dog
// Error
: String
Type unions are valid on plurals, however, the elements of type union must be either all plural, or all singular. The two cannot be mixed. For example:
// Error
Strange : Animal, Animal...
// A valid plural of rabbits who are also pets
FurryFriends : Rabbit..., Pet...
There exists the distinction between the elements in an array (typically accessed via the array[n] syntax in many programming languages), and members present on the array itself (such as the array.length property found on JavaScript arrays).
Truth also has a notion of "Types attached to plurals themselves". These types can be added to an array by moving the ellipsis operator to the has-a side of the term. We call this an On-Plural type, as opposed to an (In-Plural type). Consider the following code:
Number
Boolean
true, false : Boolean
Animal
Rabbit, Raccoon : Animal
Animals : Animal...
: Rabbit
: Raccoon
Animals...
Sort : Boolean
The above code creates a plural of Animals, and the plural itself has sorting information. (Again, note that this is just an exemplary declaration. This won't cause sorting to actually occur. It would be the responsibility of an agent to respond to this type and implement the desired behavior).
It's possible to assign both the elements of a plural as well as the types directly owned by a plural all together:
MyAnimals : Animals
// This won't generate a type error,
// even though true is a Boolean
// and not an Animal.
Sort : true
: Rabbit
: Raccoon
There are some additional rules around this syntax to avoid ambiguities. You can read about the rules around plurals in the list of [language rules](Knowledge/Language Rules.md).