dwijnand · January 23, 2023 21:02 · Jan 23, 2023
diff --git a/skolems.scala b/skolems.scala
@@ -0,0 +1,62 @@
+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 τ
No results found