Typeclass inheritance and computed members

[hacklex]

Just as the title says, I think records and typeclasses do need some love.

My motivation is, I am planning to introduce a flexible system for defining and using general algebraic structures in F*. And as we all know, relations between those are very difficult. There are lots of examples of multiple inheritance, for example.

As things currently are, if we were to start develop algebraic structures beyond the basic few, things will get ugly really quickly, and that is due to lack of language features

Here are some concrete suggestions:

• Inheritance. Best if multiple from the beginning (integral domains, commutative groups easily demands that), but can be somewhat cheaply emulated via encapsulation and magic fields. I do not know enough of F* internals to make more specific suggestions...

type magma c = {
  eq : equatable c;
  op : c -> c -> c;
  congruence : (x:c) -> (y:c) -> (z:c) -> (w:c) -> 
                        Lemma (requires eq.eq x z /\ eq.eq y w) 
                              (ensures eq.eq (op x y) (op z w))
}
type semigroup c = <[ magma c ]> {
  associativity : (x:c) -> (y:c) -> (z:c) -> 
                        Lemma (eq.eq (op (op x  y) z) (op x  (op y z)))
}
type commutative_magma c = <[ magma c ]> {
  commutativity : (x:c) -> (y:c) -> Lemma (eq.eq (x `op` y) (y `op` x))
}
type monoid c = <[ semigroup c ]> {
  neutral : c;
  identity : (x:c) -> Lemma (op x neutral `eq` x /\ op neutral x `eq` x)
}
type commutative_monoid c = <[ monoid c, commutative_magma c ]> { }

• Computed members. The idea of having extension members for some type, although usually declared outside said type if we talk C# for example, -- should be considered old nowdays, but it gives considerable expressive power.

Taste this, for example:

type ring c = {
  addition: commutative_group c;
  multiplication: (m:monoid c {m.eq == addition.eq});
  zero = addition.neutral;
  one = multiplication.neutral; // in some sources rings with mul identity are called unital rings, in some others just rings.
  mul = multiplication.op;
  eq = addition.eq.eq;
  add = addition.op;
  annihilation (x:c) : Lemma (mul x zero `eq`  zero /\ mul zero x `eq` zero) 
    = '(here goes the proof, this is a theorem for all rings regardless of c)'
}

• Perhaps propagate fields of encapsulated ("parent?") typeclasses further than just one level of encapsulation, without the need of explicitly writing instance declarations?

Maybe what I'm suggesting goes against what you guys have in mind as the philosophy of F* -- then maybe we can have some other mechanism that would (a) give us fluent syntax for declaring such objects and (b) provide us with means for solving the diamond inheritance problem (that would offer us what is called virtual inheritance in C++), allowing for example to declare a commutative group that is both a group (magma ->semigroup->monoid->) and a commutative magma (magma ->), and just from the declaration it would be immediately clear that the resulting object is a magma and there are no two (possibly different) instances of equality, or definitions of op, or anything, -- and the object will be acceptable by any function that wants a magma, a commutative magma, a semigroup, a commutative semigroup, and so on.

[nikswamy]

Hi Alex, thanks for bringing this up and congratulations on being the first user to open a discussion : )

Inheritance

Indeed, we could use some first-class support for this. Currently, inheritance among typeclasses is possible, but it requires a user-exposed encoding. See, for example: https://github.com/FStarLang/FStar/blob/master/examples/typeclasses/Num.fst#L24

Adding specialized syntax for this sounds like a good idea. You can expect something like that supported by F* soon.

[hacklex]

This is good. If it would readily emulate virtual multiple inheritance (as a solution to diamond case), it would probably give me all I might need for my algebra types

[nikswamy]

Computed members

I'm not sure I quite see the need for this. Why couldn't one just write

let annihilation (#c:Type) {| ring c |} : x:c -> Lemma (...) = fun x -> (*  here goes the proof *)

?

[hacklex]

One most certainly could :)

But I am advocating for the aesthetics offered by my_ring.annihilation elem; that underline the fact that the annihilation property is something inherent to a ring, not just a random lemma that might state something that has way more specific preconditions, depending on several different objects at once.

Especially this applies for records (not typeclasses) that do not have the similar instance resolution mechanism.

[nikswamy]

As for adding inheritance and computed members to records: I think it's unlikely that we'll go in this direction. A record is just a single constructor inductive type. Typeclasses are the way to go for the kinds of structures you're talking about, with much success in other tools for describing algebraic structures, including, e.g., in Lean.

[hacklex]

Yes. But then can we please address the issue with conflicting field names in different typeclasses?