Traits

[lukaszcz]

• Closes Juvix Type classes  #1646

Implements a basic trait framework. A simple instance search mechanism is included which fails if there is more than one matching instance at any step.

Example usage:

import Stdlib.Prelude open hiding {Show; mkShow; show};

trait
type Show A :=
  mkShow {
    show : A → String
  };

instance
showStringI : Show String := mkShow (show := id);

instance
showBoolI : Show Bool := mkShow (show := λ{x := if x "true" "false"});

instance
showNatI : Show Nat := mkShow (show := natToString);

showList {A} : {{Show A}} → List A → String
  | nil := "nil"
  | (h :: t) := Show.show h ++str " :: " ++str showList t;

instance
showListI {A} {{Show A}} : Show (List A) := mkShow (show := showList);

showMaybe {A} {{Show A}} : Maybe A → String
  | (just x) := "just (" ++str Show.show x ++str ")"
  | nothing := "nothing";

instance
showMaybeI {A} {{Show A}} : Show (Maybe A) := mkShow (show := showMaybe);

main : IO :=
  printStringLn (Show.show true) >>
  printStringLn (Show.show false) >>
  printStringLn (Show.show 3) >>
  printStringLn (Show.show [true; false]) >>
  printStringLn (Show.show [1; 2; 3]) >>
  printStringLn (Show.show [1; 2]) >>
  printStringLn (Show.show [true; false]) >>
  printStringLn (Show.show [just true; nothing; just false]) >>
  printStringLn (Show.show [just [1]; nothing; just [2; 3]]) >>
  printStringLn (Show.show "abba") >>
  printStringLn (Show.show ["a"; "b"; "c"; "d"]);

It is possible to manually provide an instance and to match on implicit instances:

f {A} : {{Show A}} -> A -> String
  | {{mkShow s}} x -> s x;

f' {A} : {{Show A}} → A → String
  | {{M}} x := Show.show {{M}} x;

The trait parameters in instance types are checked to be structurally decreasing to avoid looping in the instance search. So the following is rejected:

type Box A := box A;

trait
type T A := mkT { pp : A → A };

instance
boxT {A} : {{T (Box A)}} → T (Box A) := mkT (λ{x := x});

We check whether each parameter is a strict subterm of some trait parameter in the target. This ordering is included in the finite multiset extension of the subterm ordering, hence terminating.

[janmasrovira]

review in progress

[janmasrovira]

A big leap for Juvix 🎉