(This question is under a permanent bounty of 1000 points, once proven/refuted, it will be retrospectively set up and awarded)
(Possible duplicate: https://math.stackexchange.com/questions/4232108/%ce%bbp2-the-calculus-of-constructions-and-quantifying-over-propositions)
Considering the lambda cube:
https://en.wikipedia.org/wiki/Lambda_cube
A type system that supports both type polymorphism & dependent type:
- dependent type/type depending on term: ∀ (a: A), B
- type polymorphism/type classes/term depending on type: ∃ A, (b: B)
(assuming that a,b,c are terms, A,B,C are types)
can be classified as System λP2, a manifestation of second-order predicative logic.
On top of it, calculus of construction (CoC) also supports:
- higher-kind/type-constructor/type depending on type: A -> B
It serves as the foundation of majority of the most powerful proof assistants, including coq and LEAN4.
This extra capability appears to be useless, as any of such deduction can be rewritten into an equivalent dual form:
{ // primary
A -> B
}
{ // dual
∃ A, (g: G)
∀ (g: G), B
}
Here, the term g: G (will be referred as generic object) is only an intermediate construct that carries very little compile-time information, can be generated by the prover/compiler on the fly, and can be erased in run-time.
So why is CoC (or higher kind rules in many dependent type systems) necessary? Specifically:
- Is there an injective mapping from every proof in CoC to λP2?
- Given that dependent object type (DOT, the underlying type system of Scala 3) system is an extension of system D, which resembles λP2 but confined dependent type to path-explicit, compile-time known terms, is there an injective mapping from every Scala program to an equivalent program without higher kind?
UPDATE 1
Ideally the following examples should be formalised in a proof assistant and be posted under math/proof assistant stack exchange, but I opted to write all examples in Scala 3, a functional language with a rich type system, due to following reasons:
- Both DOT and system D has a soundness proof, while DOT with higher-kind doesn't.
- The effort to encode higher kind in Scala 3 in terms of dependent types has been attempted many times before (see the following 2016 slide):
- Status quo higher kind inference implementation of Scala 3 may be too complex and be the source of a few bugs and ambiguities (see Bugfixes section for details). Thus, the conjecture entails the immediate benefit of sidestepping them.
- I'm not a proficient user of proof assistant, neither do I have enough reputation in math/proof assistant stack exchange to set up bounties.
Regardless, I'll try to post a refined version in LEAN4 in a few weeks.
Implementation
In Scala3, there are 2 manifestations of ad-hoc type polymorphism (term depending on type): the term can either be an outer object:
object Term {
trait TT {def outer = Term.this}
}
or an implicit term summoned for the type:
trait Support[T]
trait TT
object TT {
implicit lazy val SupportTT: Support[TT] = ???
}
The following examples will only use outer object for simplicity.
Examples
Using the above convention, the most simple invariant unbounded Vec[T] can be mapped into TGen#Vec:
(Invariant with No Bound)
{ // Primary
trait Vec[T]
trait Matrix[T] extends Vec[Vec[T]]
object VInt extends Vec[Int]
object MInt extends Matrix[Int]
}
{ // Dual
trait Vec_* {
type TT
}
{ // Dual
trait Vec_* {
type TT
}
trait TGen {
type T
trait Vec extends Vec_* { type TT = T }
object VecTGen extends TGen { override type T = TGen.this.Vec }
trait Matrix extends VecTGen.Vec
}
object IntGen extends TGen { type T = Int }
object VInt extends IntGen.Vec
object MInt extends IntGen.Matrix
}
Unlike CoC, DOT supports subtyping, which introduces a few complexities, one of which is that dependent types now becomes bounds, namely type TT = T is just a shorthand of type TT >: T <: T. the complete form becomes necessary when Vec[T] has bounded argument:
(Invariant with Upper and Lower bound)
{ // Primary
trait Vec[T >: Nothing <: Any]
trait NVec[T >: Nothing <: Number] extends Vec[T]
}
{ // Dual
trait Vec_*
trait TGen {
type T_/\ <: Any
type T_\/ >: Nothing <: T_/\
trait Vec extends Vec_* { type TT >: T_\/ <: T_/\ }
}
trait NTGen extends TGen {
override type T_/\ <: Number
}
}
... or variance:
(covariant)
trait _0
trait _1 extends _0
{ // Covariant: Primary
trait Cov[+T]
type Cov_* = Cov[_]
implicitly[Cov[_1] <:< Cov[_0]]
trait G0 extends Cov[_0]
trait G1 extends G0 with Cov[_1]
object G0 extends G0
object G1 extends G1
}
{ // Dual
trait Cov_* { type TT }
trait TGen {
type T_/\
type T_\/ <: T_/\ // not used
type Cov = Cov_* { type TT <: T_/\ }
}
object _0Gen extends TGen { type T_/\ = _0; trait CovImpl extends Cov_* { type TT <: T_/\ } }
object _1Gen extends TGen { type T_/\ = _1; trait CovImpl extends Cov_* { type TT <: T_/\ } }
// boilerplate can be avoided by allowing trait to extend duck types directly
implicitly[_1Gen.Cov <:< _0Gen.Cov]
trait G0 extends _0Gen.CovImpl
trait G1 extends G0 with _1Gen.CovImpl
object G0 extends G0
object G1 extends G1
}
(Contravariant)
{ // Similarily, contravariant, Primary
trait Cov[-T]
type Cov_* = Cov[_]
implicitly[Cov[_0] <:< Cov[_1]]
}
{ // Dual
trait Cov_* {
type TT
}
trait TGen {
type T_/\ // not used
type T_\/ <: T_/\
type Cov = Cov_* { type TT >: T_\/ }
}
object _0Gen extends TGen {
type T_/\ = Any
type T_\/ = _0
}
object _1Gen extends TGen {
type T_/\ = Any
type T_\/ = _1
}
implicitly[_0Gen.Cov <:< _1Gen.Cov]
Common functional programming concepts within Hindley-Milner/System F also becomes simpler, e.g.:
(Natural number with Church encoding):
trait Nat
trait _1 extends Nat
{ // Primary
trait Succ[N <: Nat] extends Nat
type _4 = Succ[Succ[Succ[_1]]]
}
{ // Dual
trait NGen {
type _N <: Nat
trait Succ extends Nat
}
object _1 extends NGen {
type _N = _1
}
object _2 extends NGen {
type _N = _1.Succ
}
object _3 extends NGen {
type _N = _2.Succ
}
type _4 = _3.Succ
}
(Dependent poly function)
{ // Primary
sealed trait Col[V] {
trait Wrapper
val wrapper: Wrapper = ???
}
val polyFn: [C <: Col[?]] => (x: C) => x.Wrapper =
new PolyFunction {
def apply[C <: Col[?]](x: C) = x.wrapper
}
type CC = Col[_]
}
{ // Dual
trait VGen {
type V
sealed trait Col {
trait Wrapper
val wrapper: Wrapper = ???
}
}
val polyFn: [G <: VGen] => (gen: G) =>
[C <: gen.Col] => (x: C) => x.Wrapper
= ???
}
(F-bounded polymorphism)
{ // primary
trait Node[T <: Node[T]]
trait NN extends Node[NN]
}
{ // Dual
trait Node_* { type TT }
trait TGen {
type T_/\ <: NodeImpl
type T_\/ <: T_/\
type Node = Node_* { type TT >: T_\/ <: T_/\ }
trait NodeImpl extends Node_* { type TT >: T_\/ <: T_/\ }
}
object NNGen extends TGen {
type T_/\ = NN
type T_\/ = NN
}
trait NN extends NNGen.NodeImpl
}
Bugfixes
Scala3 compiler is still being actively developed and a few bugs & ambiguities were introduced due to the complexity of mixing higher kind with subtyping, they may be sidestepped or even trivialised in dual form, e.g:
(Main article From a type system perspective, In Scala 3, should variance affect extensional equality between types `F[T]` and `F[_ <: T]`?)
For a covariant higher kind in scala Mat[+T], it should be trivial to prove that Mat[Y <:< X] <:< Mat[X] for all Y <:< X by definition, and Mat[_ <: X] <:< Mat[X], but at this moment, this won't be admitted by Scala3 compiler.
(extensional equality between types F[+T] and F[+_ <: T])
{ // Primary
trait Mat[+T]
summon[Mat[Product] <:< Mat[_ <: Product]]
summon[Mat[_ <: Product] <:< Mat[Product]] // oops
summon[Mat[Product] =:= Mat[_ <: Product]] // oops
}
{ // Dual
trait Mat_* {
type TT
}
trait TGen {
type T_/\
type T_\/ <: T_/\
type Mat = Mat_* { type TT <: T_/\ }
}
object ProductGen extends TGen {
override type T_/\ = Product
override type T_\/ = Product
}
object LessThanProductGen extends TGen {
override type T_/\ = Product
override type T_\/ = Nothing
}
summon[ProductGen.Mat =:= LessThanProductGen.Mat]
}
(Main article In Scala 2 or 3, is there a higher kind argument extractor without using match type?)
(This bug has been fixed in Scala 3.4.0 https://github.com/lampepfl/dotty/issues/17149)
Match type is a Scala3 new feature equivalent to an ad-hoc type constructor, it can be reduced at compile-time to a concrete type. But its implementation is backed by complex macros which requires careful handling when combining with higher kind & variance. In the meantime, long before the existence of this feature, its dual form (using implicit term as type class) has been used in Scala2 for identical purposes, and it works flawlessly in any Scala version. For consistency, the following example will include both dual forms, using implicit terms and outer objects as type classes respectively:
(Match type extracting a covariant argument)
{ // primary
trait Vec[+T]
type Ext[S <: Vec[_]] = S match {
case Vec[t] => t
}
implicitly[Ext[Vec[Int]] =:= Int]
implicitly[Ext[Vec[Int]] <:< Int]
// broken in Scala 3.3: Cannot prove that e.Ext[Seq[Int]] =:= Int
// works in Scala 3.4+
implicitly[Int <:< Ext[Vec[Int]]]
}
{ // dual, type classes are implicit terms
trait Vec[+T]
trait SGen {
type SS
type Ext
}
type GenAux[S] = SGen { type SS = S }
object SGen {
class VecGen extends SGen {
final type SS = Vec[Ext]
}
implicit def forVec[T]: VecGen { type Ext = T } = new VecGen {
type Ext = T
}
}
val gen = summon[GenAux[Vec[Int]]]
summon[gen.Ext =:= Int] // success!
}
{ // dual, type classes are outer objects
trait Vec_* { type TT }
type VecLt[T] = Vec_* { type TT <: T } // This is unnecessary if match type can extract bound directly
trait TGen {
type T_/\
type Vec = Vec_* { type TT <: T_/\ }
}
object IntGen extends TGen {
type T_/\ = Int
}
trait SGen {
type S <: Vec_*
type Ext
}
trait VecGen extends SGen {
val tGen: TGen
type S = tGen.Vec
final type Ext = tGen.T_/\
}
object VecIntGen extends VecGen {
val tGen: IntGen.type = IntGen
}
implicitly[VecIntGen.Ext =:= Int] // success!
{ // If you insist on using match type without higher kind
trait SGen {
type S <: Vec_*
type Ext = S match {
case VecLt[t] => t
case _ => S
}
}
object SIntGen extends SGen {
final type S = Int
}
implicitly[SIntGen.Ext =:= Int]
implicitly[SIntGen.Ext <:< Int]
// still broken in Scala 3.3, but easier to fix
}
}
TL;DR
As a rule of thumb, each group of type arguments is mapped into a generic object with 2x dependent types, corresponding to upper & lower bounds respectively. I have yet to see a counterexample to this rule, and this post is already becoming too long. To incorporate it into Scala compiler (or any compiler that uses similar type systems), a formal proof for its soundness (when combined with λP2, DOT and its extensions) will be required.
So the problem becomes: what's the most realistic road map to prove or refute it, either on paper or with a machine?
UPDATE 2
I was asked if this formulation may introduce Girard's paradox, one of the many intricacies in implementing type constructors. From my limited experience playing with the compiler, it appears that Scala did a good job in avoiding it in both forms:
object Paradox {
{ // Primary
trait Vec[T]
type VV1 = List[Vec] // paradox!
type VV2 = [T] =>> Vec[T]
type NN = List[VV2] // paradox!
}
{ // Dual
trait Vec_* {
type TT
}
trait TGen {
type T
trait Vec extends Vec_* {
type TT = T
}
}
type VV2 = [TT] =>> (TGen { type T = TT })#Vec
type NN = List[VV2] // paradox!
}
}
In all 3 cases Scala gave the same error: Type argument Vec/VV2 does not have the same kind as its bound. This is obviously not a rigorous and objective validation, for which I'll need a consistent mapping of every paradoxical example from primary to dual form. Nevertheless, please point out if the formulation introduces any paradox that doesn't exist before.