Trait constraints and assumptions in Kitten

constraints.ktn

// A constraint could be sugar for a permission:
//
// “where (foo<T>)” → “+Defined(foo<T>)”
// “where (<A, B> map<F<_>, A, B>)” → “+Defined(<A, B> map<F<_>, A, B>)”
//
// It looks like effects and coeffects can both be represented with permissions because all terms are functions.

trait (<)<T> (T, T -> Bool)
trait zero<T> (-> T)
trait neg<T> (T -> T)

// Use of a trait on a generic type generates a constraint for that trait.

define abs<T> (T -> T) where ((<)<T>, neg<T>, zero<T>):
  dup  if ((< zero)) { neg }

// We need some kind of convenient way to alias groups of these. Enter constraint synonyms.

constraint Numeric<T> ((<)<T>, neg<T>, zero<T>)

define abs<T> (T -> T) where (Numeric<T>):
  dup  if ((< zero)) { neg }

// Then we can start talking about groups of traits and their laws.

// zero + x = x + zero = x
constraint Additive<T> ((+)<T>, zero<T>)

// one * x = x * one = x
constraint Multiplicative<T> ((*)<T>, one<T>)

// x * (y + z) = x * y + x * z, (x + y) * z = x * z + y * z
constraint Ring<T> (Additive<T>, Multiplicative<T>)

// This lets us express some standard typeclasses.

trait map<F<_>, A, B> (F<A>, (A -> B) -> F<B>)

constraint Functor<F<_>>:
  <A, B> map<F<_>, A, B>

trait pure<F<_>, A> (A -> F<A>)
trait (<*>)<F<_>, A, B> (F<(A -> B)>, F<A> -> F<B>)

constraint Applicative<F<_>> where (Functor<F<_>>):
  <A> pure<F<_>, A>
  <A, B> (<*>)<F<_>, A, B>

trait (>>=)<F<_>, A, B> (F<A>, (A -> F<B>) -> F<B>)

constraint Monad<F<_>> where (Applicative<F<_>>):
  <A, B> (>>=)<F<_>, A, B>

// Placing laws in metadata would let the compiler use them as rewrite rules.

about Additive<T>:
  laws:
    -> x as (T);
    (zero + x = x)
    (x + zero = x)

// Assumptions are like permissions, but attached to values rather than functions.
// Whereas a permission proves that you can grant a permission to a closure,
// assumptions prove that you can verify an assumption about a value using a dynamic or static check.
// Positive/negative permissions use * and / respectively, like permissions use + and -.

assumption Sorted<T> (List<T> -> Bool) where ((<=)<T>):
  is_sorted

// Assumptions respect variance.
// You can only pass sorted lists to this function
// but you can use the result as if it were unsorted.
define merge<T> (List<T> *Sorted, List<T> *Sorted -> List<T> *Sorted):
  …

// Similarly, you can safely pass sorted lists to this function.
define merge_sort<T> (List<T> -> List<T> *Sorted):
  …
  // A value is imbued with assumptions using the “imbue” operator.
  // We could reuse the “with” operator, but its type might need to change for clarity.
  imbue (*Sorted)

// This gives you a way to document general assumptions and have them machine-checked.
// In release mode, the dynamic checks could be removed for performance.
assumption NonEmpty<T> (List<T> -> Bool):
  empty not

// Overloads could be provided for convenience.
// For example, the head of a non-empty list is always defined.
instance head<T> (List<T> *NonEmpty -> T)