A case for contract programming in Gleam

[chouzar]

This is meant as an exploratory topic 🗺️ on how the the ideas behind contract programming could fit Gleam; below I try to make a case and summary of the pros and cons but there are not hard conclusions on any approach.

Would love anyone's thoughts 💜 on the subject and feel free to close this suggestion if its simply not a fit for the language.

Brief intro to contracts 👩‍🏫

Contracts as in contract programming is a way of defining assertions about your code. It usually looks a bit like this:

require is_numeric(num_a) and is_numeric(num_b)

fn add(num_a, num_b) {
  // our implementation goes here
  (num_a * num_b / num_b) + num_b + 1
}

ensure  result == num_a + num_b

Here the require and ensure clauses are ran at runtime; with require being checked before our implementation starts and ensure after the implementation code is finished.

• On failure the program can either throw an exception, or fail in a way that the platform knows how to manage.
• The clauses may be configured to run at test, build or runtime to have better control of guarantees/performance.

The main value here is that contracts are a simple yet powerful technique to define properties around our program, in the lack of a more thorough compiler the runtime assertions can be very helpful for identifying parts of our code that may fail.

Making the case for gleam 🌟

The main way in which Gleam helps designing programs is through types, taking an example from the guide we can define a custom type Cat like:

pub type Cat {
  Cat(name: String, cuteness: Int)
}

Which later could be used in our code as:

mew.Cat("stevie", cuteness: 1000)

But as we all know... it is impossible for a cat to have its cuteness factor below or equals to 0; sadly our program doesn't seem to account for this allowing us to do:

mew.Cat("carmelito", cuteness: -1000)

Thankfully we have ways in which we can avoid bad data!

Opaque types to the rescue 🐈

Gleam allows us to define opaque types to hinder the type manipulation and have a stricter interface:

pub opaque type Cat {
  Cat(name: String, cuteness: Int)
}

pub fn new(name, cuteness) -> Result(Cat, Indeterminate) {
    case cuteness {
        cuteness if cuteness > 0 -> {
            let cat = Cat(name, cuteness)
            Ok(cat)
        }

        _other -> 
            Error(Impossible)
    }
}

pub type Indeterminate {
    Impossible
}

By making the Cat type opaque and offering the new interface we can now safely create cats in external modules by using:

mew.new("felix", 1001)

Using cats would now require some helper functions to unwrap our Result values, this can make it hard sometimes on deciding when to draw the line between using wrappers, custom types or just try to be less strict about data.

So... contracts to the rescue? 📜

Assertions may be used in a limited fashion in Gleam to emulate contract pre or post conditions:

pub fn new(name, cuteness) -> Cat {
    // Preconditions for building a Cat
    assert True = cuteness > 0

    let cat = Cat(name, cuteness)

    // Postconditions for delivering a Cat
    assert True = cat.cuteness > 0

    cat
}

Special predicate syntax may make it easier to the eyes:

require cuteness > 0, "Should respect universal laws."
ensure  cuteness > 0, "Check implementation."

pub fn new(name, cuteness) -> Cat {
    Cat(name, cuteness)
}

Not only functions, assertions could go directly on type definitions:

pub type Cat {
    require cuteness > 0, "Should respect universal laws."
    ensure  cuteness > 0, "Check implementation."

    Cat(name: String, cuteness: Int)

    // .. Other constructors
}

More interesting properties can be found with more complex functions:

ensure result.cuteness == (cat_a.cuteness * cat_b.uteness), "Cuteness should be multiplied."
handle_as Raise                        // Handle errors as Result type, custom type or raise exception
evaluate_at [Runtime, Test, Build]     // Evaluate on specific stages

pub fn fusion(cat_a: Cat, cat_b: Cat) -> Cat {
    // ⦿⽘⦿-<  >-⦿⽘⦿
}

Also other annotation trinkets could prove useful for performance or handling failures.

Thoughts 💭

Gleam's design really tries to push on using types to its full-extent for designing programs; by adding contract programming through assertion we could add an extra layer of data integrity to our codebase, at the expense of runtime evaluation. Being a language on the BEAM maybe the "fail fast" mindset is not completely out of the question.

It is a simple system that can be expanded to a bunch of appliances, for example contracts blend well with automated tests allowing to do pseudo property testing; however it could be argued that contracts can also be too generic of a solution and that more purposely defined tools would do just as well if not better without introducing extra constructs to the language.

Contracts may also introduce some noise when used to define properties that are not really relevant, like when the assertion equals an implementation:

ensure result.cuteness == (cat_a.cuteness * cat_b.uteness)
pub fn multiply(cat_a: Cat, cat_b: Cat) -> Cat {
    cat_a.cuteness * cat_b.cuteness
}

Which feels odd and redundant, but in any case contracts would always be opt-in.

More on the topic 🤯

I'm tying too many ideas here... but wanted to add some links that intersect with the design aspects of contract programming.

On the value of "failing fast" 🤞

Not that I know these topics extensively but here are some resources (that I want to review later) on the value of "failing fast".

• Against railway oriented programming
• Offensive programming
• The Zen of erlang

Previous Gleam art 👨‍🔬

Again, libraries or extra constructs to the language may solve more on point issues and avoid feature bloat.

• Gleam validator
• Guards for external functions proposal
• Gleam tour: todo

On contracts 🤝

Other languages and ecosystems that embrace contract programming.

• Both D lang and this DbC Rust Crate seems to have a simple yet straightforward implementation of basic contracts.
• The racket and ADA communities seem to have deeper use of contracts by using it along with tools.
• Dafny is probably a great example on how contracts may evolve into more involved specifications.
• The Eiffel docs are a fun ride on how far you can take contracts since this is a language completely based around contract programming.
• Hillel's presentation "Beyond unit tests" and essays shine some light into how contracts + tests make a great combo.

[lpil]

Thanks for this write up, there's some really good information here and I've a lot to think about.

Do you envision that when a contract is violated that it returns an Error? Or that it crashes?

How much of this could be resolved at compile time? Currently we have tried to do as much statically as possible.

[chouzar]

Do you envision that when a contract is violated that it returns an Error? Or that it crashes?

From what I have seen... libraries that try to integrate contract programming into the language just throw an error at runtime, but there is not hard rule of how the program should behave on failure aside from the "fail fast" mantra. I think both, crashes and types could be provided as failure mechanisms.

For example contracts with no explicit error type would just fail the assertion and crash:

ensure result.cuteness == (cat_a.cuteness * cat_b.uteness), "bad cat arithmetic"
pub fn multiply_cutenesss(cat_a: Cat, cat_b: Cat) -> Int {
  cat_a.cuteness + cat_b.cuteness
}

While contracts may also be neatly integrated with the Result type:

pub type CatArithmeticError{
  BadArithmetic
}

ensure result.cuteness == (cat_a.cuteness * cat_b.uteness), BadArithmetic
pub fn multiply_cutenesss(cat_a: Cat, cat_b: Cat) -> Result(Int, CatArithmeticError) {
  cat_a.cuteness + cat_b.cuteness
}

And then the result of the above implementation would be wrapped either as:

• Ok(Int) or
• Error(BadArithmetic)

NOTE: Here I'm unsure what is the convention in Gleam (or other typed languages) regarding errors... make heavy use of the default Maybe types? Create your own CustomTypes? Both? 🤔

Other possibilities would be to plugin user defined parametrized types or to define an entirely different category for contract types, for which the same principle as Result could apply.

---

How much of this could be resolved at compile time? Currently we have tried to do as much statically as possible.

Yes! That would be ideal and languages/tools like Dafny seem to do very well on that regard, but it is a complete mystery to me how "totality" of contracts is achieved 🕳️.

An interesting idea here is the approach that the Typeclass elixir library takes:

TypeClass meets this challenge halfway: property testing. definst will property test a small batch of examples on every data typed that the class is defined for at compile time. By default, it skips this check in production, runs a minimal set of cases in development, and runs a larger suite in the test environment. Property testing lets TypeClass check hundreds of specific examples very quickly, so while it doesn’t give you a guarantee that your instance is correct, it does give you a high level of confidence.

Something similar could be done but for contracts themselves, but for the checks to be effective we would need to specify the data generators somehow.

[lpil]

I found some very old Rust code, seems like they used to have preconditions: https://github.com/rust-lang/rust/blob/16e4369fe3b5f00aa3cdc584a4e41c51c0d3ca8a/src/libstd/list.rs#L131

[chouzar]

Interesting! It is cool that the predicate is embedded directly on the signature, I wonder if the check is verified at compile time or just at runtime. Reminds me of guards.

It could be said that erlang and elixir guards are precondition constructs, but with current limitations they're more of a pattern matching mechanism.

Do you know what is the alt construct doing? 🤔

[lpil]

I've not found much information on it yet, but it's possibly a good one to look at.

I think alt might be the old name for match.

[chouzar]

Sorry for the long lull, nothing much to add aside from wanting to reference: https://github.com/xldenis/creusot.

An experimental contract library for rust that leans on provers to check its invariants, still on development.