Skip to content

Instantly share code, notes, and snippets.

@djspiewak
Last active October 11, 2018 17:44
Show Gist options
  • Save djspiewak/1ec5debfcd7618d05e81d8239d2ccb9e to your computer and use it in GitHub Desktop.
Save djspiewak/1ec5debfcd7618d05e81d8239d2ccb9e to your computer and use it in GitHub Desktop.
type ∀[F[_]] = scalaz.Forall[F]
/**
* An unpublished arbitrary type. May be viewed as a formulation of
* (∃ α . α). Thus, we encode a rank-1 universal by means of a rank-2
* existential. This encoding is more convenient for our purposes.
*/
sealed trait τ
object τ {
def skolemize[F[_]](fa: F[τ]): ∀[F] = new ∀[F] {
def apply[α]: F[α] = fa.asInstanceOf[F[α]]
}
def unskolemize[F[_]](fa: ∀[F]): F[τ] = fa[τ]
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment