Juvix Type classes

[jonaprieto]

We want to use type classes as follows:

class
type SemiGroup (A : Type) :=
  mkSemiGroup {
    comp : A -> A -> A;
  };

For declaring instances, use the following syntax:

instance
f : {A : Type} -> SemiGroup (List a);
f := mkSemiGroup {comp := List.comp };

use cases:

g : {A : Type} -> List A -> List A -> List A ;
g l1 l2 := comp l1 l2;

h : {A : Type} -> {{SemiGroup A}} -> A -> A;
h {{M}} a := comp {{M}} a a; -- {{M}} is not necessary. 

See the following papers:

• Implementation of type classes in Agda: https://sci-hub.mksa.top/10.1145/2034773.2034796
• Type classes in Haskell https://dl.acm.org/doi/pdf/10.1145/227699.227700

[lukaszcz]

I propose to call these traits and use trait instead of class, for two reasons:

1. Rust (and partly Scala) call them traits.
2. In my experience teaching Haskell, regardless of how much you explain this, people think that class has something to do with classes in Java and try do object-oriented programming with type classes, sometimes in ridiculously inventive and elaborate ways.