Stream: Coq users

Topic: parameterized type classes vs passing functions as arguments

walker (Mar 22 2022 at 09:03):

SF volume 4 is type classes chapter is describing parameterized type classes and I created something like this

(** ...and here is [Show] for lists: *)

Fixpoint showListAux {A : Type} (s : A -> string) (l : list A) : string :=
  match l with
    | nil => ""
    | cons h nil => s h
    | cons h t => append (append (s h) ", ") (showListAux s t)
  end.
Instance showList {A : Type} `{Show A} : Show (list A) :=
  {
    show l := append "[" (append (showListAux show l) "]")
  }.

Then I immediately noticed that we can still pass the Show property as-is to the showListAux:

Fixpoint showListAux' {A : Type} `{Show A} (l : list A) : string :=
  match l with
    | nil => ""
    | cons h nil => show h
    | cons h t => append (append (show h) ", ") (showListAux' t)
  end.


Instance showList {A : Type} `{Show A} : Show (list A) :=
{
  show l := append "[" (append (showListAux' l) "]")
}.

Is there a reason why the first style is favored over the second one ?

Paolo Giarrusso (Mar 22 2022 at 10:51):

IME, the 2nd example is the usually favored one.

Paolo Giarrusso (Mar 22 2022 at 10:54):

The difference becomes apparent if you need to call show on a xs : list A in some client. show xs works thanks to TC inference.

Paolo Giarrusso (Mar 22 2022 at 10:56):

And if you had lemmas about Show (unlikely, but you would for most other typeclasses), their statements would typically mention show. So if your term uses the instance directly, applying or rewriting with those lemmas might take more effort.

Last updated: Oct 08 2024 at 15:02 UTC