Stream: Coq users

Topic: parameterized type classes vs passing functions as arguments


view this post on Zulip 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 ?

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 10:51):

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

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC