Rules

Rules determines whether a value is valid or not, example:

// Okay, I know, 0 is neither positive nor negative
// A better name would be ZeroOrPositive
// But this is only an example
rule Positive<T: Number> { T >= 0 }

interface List<T> {
    fun get(index: Int): Option<T> where index: Positive
}

Compiler will ensure that get(int) will never be called with a negative number, also if the value is neither implicitly nor explicitly checked against a rule, an explicit check must be made. Examples:

Valid:

fun main(args) {
    val myList: List<String> = ...
    myList.get(0) // Ok
}

Invalid:

fun main(args) {
    val myList: List<String> = ...
    myList.get(-1) // Error: Value `-1` of type `Int` does not follow `Positive` rule.
}

"Implicit":

fun getIndex(): Int where return: Positive { 0 }

fun main(args) {
    val myList: List<String> = ...
    myList.get(getIndex()) // Works because getIndex specified that return value follows the 'Positive' rule.
}

"Explicit":

fun getIndex(): Int { -1 }

fun main(args) {
    val myList: List<String> = ...
    val index = getIndex()

    if (index is Positive)
        myList.get(index) // Ok
}

Or

fun getIndex(): Int { -1 }

fun main(args) {
    val myList: List<String> = ...
    
    getIndex()? Positive {
      myList.get(_)
    }

}

But the following code does not work:

fun getIndex(): Int { -1 }

fun main(args) {
    val myList: List<String> = ...
    
    myList.get(getIndex()) // Value of `getIndex()` was not checked against `Positive` rule, which is required by `List.get(int)` function.

}

Writing your own rules

First of all, you need to know that rules, from the point of view of FireflyLang, are types too, and the values that matches these rules are values of these types, from the point of view of others JVM Languages, rules are nothing, so there is no compile-time check for them, but FireflyCompiler generates bytecode verifications, so at runtime, rules are always enforced.

Rule definition

rule RULENAME<NAME: TYPE>(ARGUMENTS)* { VERIFICATION }

• RULENAME
  • Name of the rule.
• NAME
  • Name of generic declaration, this will be used as the value to check against the rule.
• TYPE
  • Type of value that rule validates.
• ARGUMENTS
  • Optional arguments. * means that ( and ) may be omitted if there is no argument.
• VERIFICATION
  • Logic that validates the value (must return a boolean).

Examples:

rule ValidFullname<T: String> { T.split(" ").all { _[0].isUpperCase() } }
rule Between<T: Comparable>(start: T, end: T) { T >= start && T <= end }
rule Negative<T: Int> { T < 0 }
rule Positive<T: Int> { T > 0 }
rule ZeroOrPositive<T: Int> { T == 0 || T is Positive }
rule ZeroOrNegative<T: Int> { T == 0 || T is Negative }

You may also define more than one pair of NAME and TYPE (Type variable), just like normal classes:

type Collection<T> {
    contains(T): Boolean
}

rule Contains<T: Collection<E>, E> { T.contains(E) }

fun <E> remove(from: Collection<E>, element: E): Boolean 
                                               where from: Contains(element) {
    ...
}

The first type variable (pair of NAME and TYPE) of a rule is the receiver, others type variables are arguments of the rule, and appear before normal arguments.

Note: The code above is only an example, you should not enforce that an element is present on a collection to remove it.

Custom rule messages

TODO

Safe index access with rules

Now we will show how to write a vector with safe index access.

Declarations

rule Between<T: Comparable>(start: T, end: T) { T >= start && T <= end }

class Vector<T, S: 'Int>(private val array: Array<T>) {
  
  fun <T> new(): Vector<T, 0> =
      new(Array.new(0))

  fun <T> new(T): Vector<T, 1> =
      new(Array.new(1, _))

  fun get(index: Int): T where index: Between(0, S-1) = array.get(index)

  fun set(index: Int, T): T where index: Between(0, S-1) =
    array.set(index, T)

  fun +(T): Vector<T, S + 1> =
      Vector.new(this.array + _)

  fun -(T): Vector<T, S - 1> =
      Vector.new(this.array - _)
  
  fun :(): Seq<T> = this.array.toSeq()

  fun [](index: Int) = this.get(index)
}

Usage

Lets see what happens if we tries to access an element at the index 0 of a empty vector.

Code:

val names = Vector.new<String>() // Vector<String, 0>
names[0]

Output:

Error: Value `0` of type `Int` does not follow `Between(0, -1)` rule.

But this code works:

val names = Vector.new() + "Firefly" + "Rules" // Vector<String, 2>
names[0]
names[1]

We could also improve our rule to achieve better error messages or use InRange rule, example:

...
  fun get(index: Int): T where index: InRange(0, S) = array.get(index)

Trying to access a out of bounds index would result in following error:

Range(0, 0) does not contains value 5.

TODO