skolems.scala

package skolems

import scala.language.implicitConversions

trait Exists[+F[_]] extends Serializable:
  type A
  val value: F[A]

trait Forall[+F[_]] extends Serializable:
  def apply[A]: F[A]

object Exists extends IdentityPartials:
  // A forgetful constructor which packs a concrete value into an existential.
  // This is mostly useful for explicitly assisting the compiler in sorting all of this out.
  def apply[F[_]]: PartiallyApplied[F] = new PartiallyApplied[F]
  final class PartiallyApplied[F[_]]:
    def apply[A0](fa: F[A0]): Exists[F] = new Exists[F]:
      type A = A0
      val value = fa

  // Tricksy overload for when you want everything to "just work(tm)".
  // The implicit modifiers are to allow the compiler to materialize things through implicit search when relevant;
  // don't be afraid to call this function explicitly.
  implicit def apply[F[_], A](implicit fa: F[A]): Exists[F] = apply[F](fa)

  // non-implicit parameter version designed to provide nicer syntax
  implicit def coerce[F[_], A](F: F[A]): Exists[F] = apply(F)
end Exists

abstract class Identities:
  def raiseA[F[_], B](f: ∀[[a] =>> F[a] => B]) : ∃[[a] =>> F[a]] => B = ef => f[ef.A](ef.value)
  def raiseE[F[_], B](f: ∃[[a] =>> F[a] => B]) : ∀[[a] =>> F[a]] => B = af => f.value(af[f.A])
  //           ---- raise --->
  // ∀a =>> F a => b === (∃a =>> F a) => b
  // ∃a =>> F a => b === (∀a =>> F a) => b
  //           <--- lower ----
  def lowerA[F[_], B](f: ∃[[a] =>> F[a]] => B) = ∀[[a] =>> F[a]  => B]((ft: F[τ]) => f(∃[[a] =>> F[a]](ft)))
  def lowerE[F[_], B](f: ∀[[a] =>> F[a]] => B) = ∃[[a] =>> F[a]  => B]((ft: F[τ]) => f(∀[[a] =>> F[a]](ft)))

abstract class IdentityPartials extends Identities:
  def lowerAP[F[_], B] = new LowerAP[F, B]
  def lowerEP[F[_], B] = new LowerEP[F, B]
  final class LowerAP[F[_], B] { def apply[A](f: ∃[[a] =>> F[a]] => B)  : F[A] => B  = lowerA[F, B](f)[A]    }
  final class LowerEP[F[_], B] { def apply   (f: ∀[[a] =>> F[a]] => B)/*: F[a] => B*/= lowerE[F, B](f).value }

object Forall extends IdentityPartials:
  // This function is intended to be invoked explicitly,
  // the implicit modifiers are simply because the compiler can infer this in many cases.
  // For example, the below will work:
  //    implicit def eitherMonad[A]: Monad[Either[A, ?]] = ???
  //    implicitly[∀[α => Monad[Either[α, ?]]]]
  def apply[F[_]](ft: F[τ]): Forall[F] = new Forall[F]:
    def apply[A] = ft.asInstanceOf[F[A]]
end Forall

type ∀[+F[_]] = Forall[F]
val ∀ = Forall

type ∃[+F[_]] = Exists[F]
val ∃ = Exists

private[skolems] type τ