Currying using canonical structures

Currying.v

Require Import List.

Module Currying.
  Record class (Dom : Type) (Curr : Type -> Type) :=
         Class { Fun : forall cod, Curr cod -> (Dom -> cod) }.
  Structure type := Pack { dom      : Type
                         ; curr     : Type -> Type
                         ; class_of : class dom curr }.
  Definition flippedmap (Curry : type) :
    forall cod, list (dom Curry) -> curr Curry cod -> list cod.
    refine (let 'Pack _ _ (Class fc) := Curry
            in fun cod xs f => List.map _ xs) ; apply fc, f.
  Defined.
  Arguments flippedmap {Curry} {cod} f xs.
  Arguments Class {Dom} {Curr} Fun.

  Module theory.
  Notation "f <$> xs" := (flippedmap xs f) (at level 70).
  End theory.
End Currying.

Import Currying.theory.

Definition pair_curry (c1 c2 : Currying.type) :
           forall cod, Currying.curr c1 (Currying.curr c2 cod) ->
                       (Currying.dom c1 * Currying.dom c2) -> cod.
  intros cod f (a, b).
  apply c2 ; [| exact b].
  apply c1 ; [| exact a].
  exact f.
Defined.


Canonical Structure CurryingPair (c1 : Currying.type) (c2 : Currying.type) : Currying.type :=
  Currying.Pack (Currying.dom c1 * Currying.dom c2)
                (fun cod => Currying.curr c1 (Currying.curr c2 cod))
                (Currying.Class (pair_curry c1 c2)).

Canonical Structure failsafe (a : Type) : Currying.type :=
  Currying.Pack a (fun cod => a -> cod) (Currying.Class (fun _ f => f)).

Check ((fun x => 2 * x) <$> (cons 1 (cons 2 nil))).
Eval compute in ((fun x => 2 * x) <$> (cons 1 (cons 2 nil))).
Check ((fun x y => x) <$> (cons (1, 2) (cons (2, 3) nil))).
Eval compute in ((fun x y => x) <$> (cons (1, 2) (cons (2, 4) nil))).

Definition map_pair {A B C} (f : A -> B -> C) (l : list (A * B)) : list C := f <$> l.
Definition map_triple {A B C D} (f : A -> B -> C -> D) (l : list (A * B * C)) : list D := f <$> l.
Definition map_quad {A B C D E} (f : A -> B -> C -> D -> E) (l : list (A * B * C * D)) : list E := f <$> l.

Definition map_nestedpairs {A B C D E} (f : A -> B -> C -> D -> E) (l : list ((A * B) * (C * D))) : list E := f <$> l.