TB-Docs/research/02_syntax_revision.md

Syntax Revision

Following the first draft of the syntax (see below), some improvements were necessary, especially to better follow the principle of least surprise and more closely map to existing Python syntax.

First draft

This was the first draft for the custom syntax:

// Simple custom type derived from floats
type Latitude<float>
type Longitude<float>

// Complex custom type, containing two values accessible through properties
type GeoLocation<Latitude, Longitude> {
    lat: Latitude
    lon: Longitude
}

type LatitudeDiff<float>
type LongitudeDiff<float>

// Simple operation defined on our custom types
op <Latitude> - <Latitude> = <LatitudeDiff>
op <Longitude> - <Longitude> = <LongitudeDiff>

// Simple custom type with a constraint
type Age<int + (0 <= _) + (_ < 150)>

// Predefined custom constraints that can be referenced in other definitions
constraint Positive = _ >= 0
constraint StrictlyPositive = _ > 0

Several issues were highlighted:

• <...> is generally used for generic templates, not type sub-typing. It is also not a Pythonic syntax at all
• GeoLocation<Latitude, Longitude> is can be confusing. It could either be interpreted as a tuple or a type union
• Defining property types both in the bases and as type hints on the properties is redundant
• op <...> - <...> = <...> is not a very standard syntax and is definitely surprising for Python users
• LatitudeDiff<float and LongitudeDiff<float> might be better expressed using a generic Difference type
• type Age<int + (0 <= _) + (_ < 150)> is mixing multiple concerns into an intricate syntax, might be unclear / hard to decipher

Revision

The syntax was revised with the following changes:

• Use DerivedType(BaseType) to defined types, more closely matches Python inheritance
• Use a new where keyword to add constraints on types
• Add generic types type Name[TypeVar](BaseType)
• Complex generics (i.e. generics with a complex template type) must be explicitly defined to specify how its properties are derived
• Remove complex type bases, only keep property types
• Move operation definitions in an extend block
• Use dunder methods (e.g. __sub__) to define operations with builtin operators to match Python syntax
• Use -> ReturnType for operation return types
• Change constraint definition to be more functional:
  • Use predicate keyword instead of constraint
  • Explicitly define value type
  • Allow predicate parameter aliases to improve readability
• Add notation for nullable types, e.g. int?. This doesn't correspond to Python's Optional but is easier to write, yet still clear

Here are some example statements using the revised syntax:

// Simple custom type derived from float
type Custom(float)

// Simple custom types with constraints
type Latitude(float) where (-90 <= _ <= 90)
type Longitude(float) where (-180 <= _ <= 180)

// Generic custom type (a Difference of T is derived from T, e.g. a difference of floats is a float
type Difference[T](T)

// Complex custom type, containing two values accessible through properties
type GeoLocation {
    lat: Latitude
    lon: Longitude
}

// Define operations on our custom type
extend GeoLocation {
    // This type is compatible with the `-` operation with another GeoLocation
    // i.e. you can subtract a GeoLocation from another GeoLocation, resulting
    // in a Difference of GeoLocations
    op __sub__(GeoLocation) -> Difference[GeoLocation]
}

// For complex generics, you need to specify how the genericity the properties
// are handled
type Difference[GeoLocation] {
    lat: Difference[Latitude]
    lon: Difference[Longitude]
}

// Simple operation defined on our custom types
extend Latitude {
    op __sub__(Latitude) -> Difference[Latitude]
}

extend Longitude {
    op __sub__(Longitude) -> Difference[Longitude]
}

// Predefined custom predicates that can be referenced in other definitions
predicate Positive(v: float) = v >= 0
predicate StrictlyPositive(v: float) = v > 0
predicate Equatorial(loc: GeoLocation) = (-10 <= loc.lat <= 10)
predicate Arctic(loc: GeoLocation) = (loc.lat >= 66)

type Person {
    name: str

    // Property with an inline constraint
    age: int? where (0 <= _ < 150)

    // Property referencing a predicate
    height: float where StrictlyPositive

    home: GeoLocation
}

The syntax should also allow defining types as refinements of complex types. In most cases, these will only provide type refinements and not structural extensions, i.e. user will not need to add new properties, only new constraints.

The following are some of the proposed syntaxes:

// Explicit, but new keyword
type EquatorialPerson refines Person where Equatorial(_.home)

// Explicit with existing keyword, might be confusing if expectations regarding 'is'
type EquatorialPerson is Person where Equatorial(_.home)

// Consistent and Python-friendly but can be confused with structural extension
type EquatorialPerson(Person) where Equatorial(_.home)

// Allow new properties, probably not useful
type EquatorialPerson extends Person where Equatorial(_.home)

Discussion points

Some points are not yet well defined, mainly how generics should be defined and handled, and as explained above, how complex type refinements should be written.