Constraining generic types arguments

[KtorZ]

While working on the standard library today, we realize that we currently have no ways to specify basic constraints on generic types. For example, how to implement a sort function on generic lists?

fn sort(xs : List(a)) -> List(a) {
    ?
}

An option is to basically "do nothing" with the compiler and inline the constraint as argument, for example:

fn sort(compare : fn(a,a) -> Comparable, xs : List(a)) -> List(a) {
   ...
}

but this is sub-optimal because quite noisy for the developer. We might want to explore a concept of Trait or Type-Class for tacking this nicely.

[rvcas]

pub trait Eq {
  fn eq(left: a, right: a) -> Bool
}

pub type Ordering {
  Less
  Greater
  Equal
}

pub trait Ord {
  fn compare(left: a, right: a) -> Ordering
}

impl Eq for Int {
  fn eq(left: Int, left: Int) -> Int {
    left == right
    // or do we match on: compare(left, right)
    // if `==` will work on anything with `Eq` would the above be recursive
  }
}

// pub type Tree<a: Eq & Ord> {
pub type Tree<a> where a: Eq & Ord {
  Empty

  Node { data: a, left: Tree, right: Tree }
}

pub fn insert(
  tree: Tree<data>,
  data new_data: data,
) -> Tree<data> where data: Eq & Ord {
  when tree is {
    Empty -> leaf(new_data)
    Node { data, left, right } ->
      // or should we just do this: when compare(new_data, data) is
      if new_data < data {
        Node { data, left: insert(left, new_data, cmp), right }
      } else if new_data > data {
        Node { data, left, right: insert(right, new_data, cmp) }
      } else {
        tree
      }
  }
}

some idea for traits in aiken

[KtorZ]

Minor remark: does pub makes sense in front of trait? I'd expect traits (at least, those ones) to always be public.

[rvcas]

We can probably omit pub and have them always be public. I was just borrowing some rust syntax.

[KristianBalaj]

This would be useful. I would immediately write custom Eq trait for Value comparing the amounts. I don't believe the invariants of Value that it doesn't ever keep the 0 amount asset and so breaks comparisons.
Especially in smart contracts, I want to be absolutely sure and even check for possible abnormalities.

[KtorZ]

@KristianBalaj I don't believe the invariants of Value that it doesn't ever keep the 0 amount asset and so breaks comparisons.

What makes you think that? Do you have any counter-example?

[KristianBalaj]

I don't have any example. I've just managed to do it on a different ledger implementation that doesn't force some constraints on Values like min ADA. So I was able to consume UTXO with 0 ADA and when I've used such input with the stdlib so it was keeping the 0 ADA in there and was breaking comparisons.
Of course, it's a special case that doesn't influence a real world scenario, but I have concerns that Ledger could theoretically send Value with 0 amount asset which would break the code, maybe not now but in some future version.

Maybe I'm just being too paranoid, but I want to be 100% sure the comparisons are correct.

[KtorZ]

This is impossible in PlutusV2 as the context and the translation of a transaction into it is bound to a specific Plutus version. For Value in particular, the protocol also guarantee we have a non-zero Ada amount anyway because of the minimum deposit required on all output.

So this might be possible in future versions of Plutus indeed, but we will have to adapt the stdlib anyway because of new fields in the script context and whatnot. So implicitly, versions of the stdlib are also bound to specific Plutus version, we might want to advertise that more explicitly.

[MicroProofs]

I've added most of the scaffolding in code gen to support traits for types. It would mainly be now adding it to the front end of the compiler and then hooking it up to code gen at this point. Not a small task, but a lot of progress has been made.

[MicroProofs]

Bump for last message to be seen.