Language Walk Through

paulgo edited this page Nov 7, 2018 · 8 revisions

Language Walk Through

Genesis

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)

A Powerful Language With Just 1 Operator

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.

Building A Language From A Blank Slate

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.

Anonymous Types

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.

Type Inference

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

Fresh Types

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

Type Unions

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:

Fragmented Types

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

Covariant Types

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

Deeply Nested Types

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.

Dependent Types

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.

Plurals

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... 

In And On

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).

You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.