build.sbt

// The simplest possible sbt build file is just one line:

scalaVersion := "2.13.3"
// That is, to create a valid sbt build, all you've got to do is define the
// version of Scala you'd like your project to use.
addCompilerPlugin("org.typelevel" % "kind-projector" % "0.11.3" cross CrossVersion.full)

// ============================================================================

// Lines like the above defining `scalaVersion` are called "settings". Settings
// are key/value pairs. In the case of `scalaVersion`, the key is "scalaVersion"
// and the value is "2.13.3"

// It's possible to define many kinds of settings, such as:

name := "hello-world"
organization := "ch.epfl.scala"
version := "1.0"

// Note, it's not required for you to define these three settings. These are
// mostly only necessary if you intend to publish your library's binaries on a
// place like Sonatype or Bintray.


// Want to use a published library in your project?
// You can define other libraries as dependencies in your build like this:

libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2"

// Here, `libraryDependencies` is a set of dependencies, and by using `+=`,
// we're adding the scala-parser-combinators dependency to the set of dependencies
// that sbt will go and fetch when it starts up.
// Now, in any Scala file, you can import classes, objects, etc., from
// scala-parser-combinators with a regular import.

// TIP: To find the "dependency" that you need to add to the
// `libraryDependencies` set, which in the above example looks like this:

// "org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2"

// You can use Scaladex, an index of all known published Scala libraries. There,
// after you find the library you want, you can just copy/paste the dependency
// information that you need into your build file. For example, on the
// scala/scala-parser-combinators Scaladex page,
// https://index.scala-lang.org/scala/scala-parser-combinators, you can copy/paste
// the sbt dependency from the sbt box on the right-hand side of the screen.

// IMPORTANT NOTE: while build files look _kind of_ like regular Scala, it's
// important to note that syntax in *.sbt files doesn't always behave like
// regular Scala. For example, notice in this build file that it's not required
// to put our settings into an enclosing object or class. Always remember that
// sbt is a bit different, semantically, than vanilla Scala.

// ============================================================================

// Most moderately interesting Scala projects don't make use of the very simple
// build file style (called "bare style") used in this build.sbt file. Most
// intermediate Scala projects make use of so-called "multi-project" builds. A
// multi-project build makes it possible to have different folders which sbt can
// be configured differently for. That is, you may wish to have different
// dependencies or different testing frameworks defined for different parts of
// your codebase. Multi-project builds make this possible.

// Here's a quick glimpse of what a multi-project build looks like for this
// build, with only one "subproject" defined, called `root`:

// lazy val root = (project in file(".")).
//   settings(
//     inThisBuild(List(
//       organization := "ch.epfl.scala",
//       scalaVersion := "2.13.3"
//     )),
//     name := "hello-world"
//   )

// To learn more about multi-project builds, head over to the official sbt
// documentation at http://www.scala-sbt.org/documentation.html

main.scala

// This is Yoneda's lemma in Scala,
// which is an exceprt from https://www.slideshare.net/100005930379759/scala-scala
// with slight modification

object Main extends App {
  // F[_] for object mapping and map() for morphism mapping 
  trait EndoFunctor[F[_]] {
    def map[X, Y](f: X => Y): F[X] => F[Y]
  }
  // Pick a functor implementation by specifying Kind
  object EndoFunctor {
    def apply[F[_]](implicit instance: EndoFunctor[F]) : EndoFunctor[F] = instance
  }
  // Natural transformation: F and G are functors
  trait ~>[F[_], G[_]] {
    def apply[X](x: F[X]):G[X]
  }
  // Seq functor
  implicit val seqFunctor = new EndoFunctor[Seq] {
    def map[X, Y](f: X => Y): Seq[X] => Seq[Y] = _.map(f)
  }
  // Const functor: always mapping to the specific object and the specific morphism
  type Const[X] = Int
  implicit val constFunctor = new EndoFunctor[Const] {
    def map[X,Y](f: X => Y): Const[X] => Const[Y] = x => x // always mapping to an identity morphism
  }
  // a natural transformation from Seq functor to Const functor
  val length = new (Seq ~> Const) {
    def apply[X](x: Seq[X]): Const[X] = x.length
  }
  // a morphism mapped by functors
  val f: Int => String = x => s"$x"
  // Verify commutativity
  println( length(EndoFunctor[Seq].map(f)(Seq(0, 1, 2))) )
  println( EndoFunctor[Const].map(f)(length(Seq(0, 1, 2))) )

  // Yoneda's lemma
  type Hom[X, Y] = X => Y
  // Without kind-projector, Hom[X, *] should be written as like ({type HomXTo[Y] = Hom[X, Y]})#HomXTo
  def liftY[F[_], X](x: F[X])(implicit F: EndoFunctor[F]): Hom[X, *] ~> F =
    new (Hom[X, *] ~> F) {
      def apply[A](f: Hom[X, A]): F[A] = EndoFunctor[F].map(f)(x)
    }
  def lowerY[F[_], X](f: Hom[X, *] ~> F): F[X] = f(x => x)


  println( lowerY(liftY(Seq(0, 1, 2))) )
}

yoneda.cpp

// This is Yoneda's lemma in C++11?
// which is derived from one in Scala by https://www.slideshare.net/100005930379759/scala-scala

#include <functional>
#include <algorithm>
#include <vector>
#include <iostream>
#include <string>

// (generic) function type is verbose in C++
template<typename X, typename Y>
using Hom = std::function<Y(X)>;

// mapOb<X> for object mapping and map() for morphism mapping 
#if 0 // not used actually, may become concept in C++20
template<template <typename> class F>
struct EndoFunctor
{
    template<typename X>
    using mapOb = F<X>;
    template<typename X, typename Y>
    Hom<mapOb<X>,mapOb<Y>> map(Hom<X,Y> f) const;
};
#endif

// Natural transformation: F and G are functors
// may become concept in C++20
// used to define type aliases
template<typename F, typename G>
struct Nat_
{
    using FunctorF = F;
    using FunctorT = G;
    template<typename X>
    using mapObF = typename FunctorF::template mapOb<X>;
    template<typename X>
    using mapObT = typename FunctorT::template mapOb<X>;
//  template<typename X>
//  mapObT<X> operator()(mapObF<X>) const;
};

// Seq functor
template<typename T>
using Seq = std::vector<T>;
struct SeqFunctor // : EndoFunctor<Seq>
{
    template<typename X>
    using mapOb = Seq<X>;
    template<typename X, typename Y>
    Hom<mapOb<X>,mapOb<Y>> map(Hom<X,Y> f) const {
        return [f](mapOb<X> x){
            mapOb<Y> y(x.size());
            std::transform(x.begin(), x.end(), y.begin(), f);
            return y;
        };
    }
};

// Const functor: always mapping to the specific object and the specific morphism
#if 1
template<typename T>
struct Const
{
    Const(int n):n(n) {}
    operator int() const { return n; }
    int n;
};
#else
// GCC rejects by invalid use of incomplete type ‘class std::function<Const<Y>(Const<X>)>’
// while CLANG accepts
template<typename T>
using Const = int;
#endif

struct ConstFunctor // : EndoFunctor<Const>
{
    template<typename X>
    using mapOb = Const<X>;
    template<typename X, typename Y>
    Hom<mapOb<X>,mapOb<Y>> map(Hom<X,Y> f) const {
        return [](mapOb<X> x){ return mapOb<Y>(x); };
    }
};

// a natural transformation from Seq functor to Const functor
struct length_ : Nat_<SeqFunctor, ConstFunctor>
{
    template<typename X>
    Const<X> operator()(Seq<X> x) const { return x.size(); }
} length;
// a morphism mapped by functors
Hom<int, std::string> f = [](int i){ return std::to_string(i); };

// Yoneda's lemma
//template<typename X>
//struct HomBind
//{
//    template<typename Y>
//    using Hom1 = Hom<X, Y>;
//};
template<typename X>
struct HomFunctor // : EndoFunctor<HomBind<X>::template Hom1>
{
    using dom = X;
    template<typename A>
    using mapOb = Hom<X,A>;
    template<typename A, typename B>
    Hom<mapOb<A>,mapOb<B>> map(Hom<A,B> f) const
    {
        return [f](mapOb<A> xa){ return [f,xa](X x){ return f(xa(x)); }; };
        //                                                  ~~~~~~~~ b in B
        //                              ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ mapOb<B> = Hom<X,B>
    }
};

template<typename X, typename F>
struct LiftY : Nat_<HomFunctor<X>, F>
{
    LiftY(typename F::template mapOb<X> x) : x(x) {}
    template<typename A>
    typename F::template mapOb<A> operator()(Hom<X,A> f) const {
        return F().map(f)(x);
    }
    typename F::template mapOb<X> x;
};

template<typename X, typename F>
LiftY<X, F>
liftY(typename F::template mapOb<X> x)
{
    return LiftY<X, F>(x);
}
// NatHomX2F has I/F like template<typename X, typename F> Nat_<HomFunctor<X>, F>
// may be bound by concept in C++20
template<typename NatHomX2F>
typename NatHomX2F::FunctorT::template mapOb<typename NatHomX2F::FunctorF::dom> lowerY(NatHomX2F f)
{
    using X = typename NatHomX2F::FunctorF::dom;
    Hom<X, X> idX = [](X x){ return x; };
    return f(idX);
}

int main(void)
{
    // Verify commutativity
    std::cout << length(SeqFunctor().map(f)(Seq<int>{0, 1, 2})) << std::endl;
    std::cout << ConstFunctor().map(f)(length(Seq<int>{0, 1, 2})) << std::endl;

    // Yoneda's lemma
    for(auto &v: lowerY(liftY<int, SeqFunctor>(Seq<int>{0,1,2}))) {
        std::cout << v << ' ';
    }
    std::cout << std::endl;

    return 0;
}

yoneda.cpp20.cpp

// This is Yoneda's lemma in C++20?
// which is derived from one in Scala by https://www.slideshare.net/100005930379759/scala-scala

#include <functional>
#include <algorithm>
#include <vector>
#include <iostream>
#include <string>
#include <concepts>

// (generic) function type is verbose in C++
template<typename X, typename Y>
using Hom = std::function<Y(X)>;

namespace { // arbitrary types
    class XX;
    class YY;
}

// mapOb<X> for object mapping and map() for morphism mapping 
template<typename F>
concept EndoFunctor = requires(XX xx, YY yy) {
    typename F::template mapOb<XX>;
    { std::declval<const F>().map(std::declval<Hom<XX, YY>>()) }
    -> std::same_as<Hom<typename F::template mapOb<XX>, typename F::template mapOb<YY>>>;
};

// Natural transformation: F and G are functors
template<typename T, typename F, typename G>
concept Nat = EndoFunctor<F> && EndoFunctor<G> &&
    requires(XX xx)
{
    typename T::FunctorF;
    requires std::same_as<typename T::FunctorF, F>;
    typename T::FunctorT;
    requires std::same_as<typename T::FunctorT, G>;
    typename T::template mapObF<XX>;
    requires std::same_as<
        typename T::template mapObF<XX>,
        typename F::template mapOb<XX>>;
    typename T::template mapObT<XX>;
    requires std::same_as<
        typename T::template mapObT<XX>,
        typename G::template mapOb<XX>>;
    { std::declval<const T>()(std::declval<typename T::template mapObF<XX>>()) }
    -> std::same_as<typename T::template mapObT<XX>>;
};
// used to define type aliases
template<EndoFunctor F, EndoFunctor G>
struct NatHelper
{
    using FunctorF = F;
    using FunctorT = G;
    template<typename X>
    using mapObF = typename FunctorF::template mapOb<X>;
    template<typename X>
    using mapObT = typename FunctorT::template mapOb<X>;
};

// Seq functor
template<typename T>
using Seq = std::vector<T>;
struct SeqFunctor
{
    template<typename X>
    using mapOb = Seq<X>;
    template<typename X, typename Y>
    Hom<mapOb<X>,mapOb<Y>> map(Hom<X,Y> f) const {
        return [f](mapOb<X> x){
            // C++20 range is not so helpful here because container I/F is still iterator base
            mapOb<Y> y(x.size());
            std::transform(x.begin(), x.end(), y.begin(), f);
            return y;
        };
    }
};

// Const functor: always mapping to the specific object and the specific morphism
#if 1
template<typename T>
struct Const
{
    Const(int n):n(n) {}
    operator int() const { return n; }
    int n;
};
#else
// GCC rejects by like invalid use of incomplete type ‘Hom<Const<X>, Const<Y>>’
// while CLANG accepts
template<typename T>
using Const = int;
#endif

struct ConstFunctor
{
    template<typename X>
    using mapOb = Const<X>;
    template<typename X, typename Y>
    Hom<mapOb<X>,mapOb<Y>> map(Hom<X,Y> f) const {
        return [](mapOb<X> x){ return mapOb<Y>(x); };
    }
};

// a natural transformation from Seq functor to Const functor
struct length_ : NatHelper<SeqFunctor, ConstFunctor>
{
    template<typename X>
    Const<X> operator()(Seq<X> x) const { return x.size(); }
} length;
// a morphism mapped by functors
Hom<int, std::string> f = [](int i){ return std::to_string(i); };

// Yoneda's lemma
template<typename X>
struct HomFunctor
{
    using dom = X;
    template<typename A>
    using mapOb = Hom<X,A>;
    template<typename A, typename B>
    Hom<mapOb<A>,mapOb<B>> map(Hom<A,B> f) const
    {
        return [f](mapOb<A> xa){ return [f,xa](X x){ return f(xa(x)); }; };
        //                                                  ~~~~~~~~ b in B
        //                              ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ mapOb<B> = Hom<X,B>
    }
};

template<typename X, EndoFunctor F>
struct LiftY : NatHelper<HomFunctor<X>, F>
{
    LiftY(typename F::template mapOb<X> x) : x(x) {}
    template<typename A>
    typename F::template mapOb<A> operator()(Hom<X,A> f) const {
        return F().map(f)(x);
    }
    typename F::template mapOb<X> x;
};

template<typename X, EndoFunctor F>
LiftY<X, F>
liftY(typename F::template mapOb<X> x)
{
    return LiftY<X, F>(x);
}
template<typename NatHomX2F>
  requires Nat<NatHomX2F, typename NatHomX2F::FunctorF, typename NatHomX2F::FunctorT>
  && std::same_as<
    typename NatHomX2F::FunctorF::template mapOb<XX>,
    typename HomFunctor<typename NatHomX2F::FunctorF::dom>::template mapOb<XX>>
typename NatHomX2F::FunctorT::template mapOb<typename NatHomX2F::FunctorF::dom> lowerY(NatHomX2F f)
{
    using X = typename NatHomX2F::FunctorF::dom;
    Hom<X, X> idX = [](X x){ return x; };
    return f(idX);
}

int main(void)
{
    // Verify commutativity
    std::cout << length(SeqFunctor().map(f)(Seq<int>{0, 1, 2})) << std::endl;
    std::cout << ConstFunctor().map(f)(length(Seq<int>{0, 1, 2})) << std::endl;

    // Yoneda's lemma
    for(auto &v: lowerY(liftY<int, SeqFunctor>(Seq<int>{0,1,2}))) {
        std::cout << v << ' ';
    }
    std::cout << std::endl;

    return 0;
}

yoneda.v

(* This is Yoneda's lemma in Coq? *)
(* which is derived from one in Scala by https://www.slideshare.net/100005930379759/scala-scala *)
(* NOTE that this is not a proof, but just an implication inside programming language *)

Require Import List String Ascii.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Import ListNotations.

(* f for object mapping and fmap for morphism mapping *)
(* ref. https://github.com/jwiegley/coq-haskell/blob/master/src/Data/Functor.v *)
Class EndoFunctor (f : Type -> Type) : Type := {
    fmap : forall {a b : Type}, (a -> b) -> f a -> f b
}.

(* Natural transformation: F and G are functors *)
Class Nat {f: Type -> Type} (F : EndoFunctor f) {g: Type -> Type} (G : EndoFunctor g) : Type := {
    trans : forall {x : Type}, (f x) -> (g x)
}.
Notation "F ~> G" := (Nat F G) (at level 28, left associativity, only parsing).

(* Seq functor *)
Instance SeqFunctor : EndoFunctor list := {
    fmap _ _ f l := List.map f l
}.

(* Const functor: always mapping to the specific object and the specific morphism *)
Definition const (X: Type) := nat.
Instance ConstFunctor : EndoFunctor const := {
    fmap _ _ _ := fun x => x
}.

(* a natural transformation from Seq functor to Const functor *)
Instance Length : SeqFunctor ~> ConstFunctor := {
    trans _ l := List.length l 
}.

(* from https://coq.inria.fr/library/Coq.Strings.String.html *)
Fixpoint string_of_list_ascii (s : list ascii) : string
  := match s with
     | nil => EmptyString
     | cons ch s => String ch (string_of_list_ascii s)
     end.

(* a morphism mapped by functors *)
Open Scope char_scope.
Definition myf x := string_of_list_ascii (repeat "X" x).

Definition seq := [1;2;3].

(* Verify commutativity for specific instance *)
Goal trans (fmap myf seq) = fmap myf (trans seq).
Proof.
    auto.
Qed.

(* Verify commutativity *)
Goal forall x, trans (fmap myf x) = fmap myf (trans x).
Proof.
    induction x.
    - simpl. reflexivity.
    - simpl. simpl in IHx. rewrite IHx. reflexivity.
Qed.

(* Yoneda's lemma *)
Definition liftY {F: Type -> Type} (FF: EndoFunctor F) {X: Type} (x: F X) :=
    fun A => fun f: X -> A => @fmap F FF X A f x.

Definition lowerY {F: Type -> Type} (FF: EndoFunctor F) {X: Type} (f: forall A, (X -> A) -> F A) :=
    f X (fun x => x).

(* for specific instance *)
Goal seq = (lowerY _ (liftY _ seq)).
Proof.
    auto.
Qed.

(* for list nat, which means SeqFunctor and nat *)
Theorem lowerY_liftY_id:  forall l: list nat, l = (lowerY _ (liftY _ l)).
Proof.
    induction l.
    - auto.
    - unfold liftY in *. unfold lowerY in *.
      simpl in *. rewrite <- IHl. reflexivity.
Qed.

(* for inverse, too difficult for me *)
Goal forall n :(forall A, (nat -> A) -> list A), forall f,
    n nat f = (liftY _ (lowerY _ n)) nat f.
Proof.
    intros.
    unfold lowerY. unfold liftY.
    simpl.
    (* stucked at
       n nat f = map f (n nat (fun x : nat => x)) *)
Admitted.