Types with universal quantifiers
Nov. 19th, 2022 01:28 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
chaourceTypes with universal quantifiers correspond to "generic functions", that is, functions with a type parameter (or with several type parameters). For example (Scala):
def f[A]: (A, Option[A]) => Option[(A, A)] = {
case (x, oy) => oy.map(y => (x, y))
}
In a more mathematical type notation, the function f has type ∀A. A × (1 + A) → 1 + A × A.
The programmer's intuition for generic functions is that these functions work in the same way for all types. Indeed, the code of f does not depend on the type A and works in the same way for all A.
The requirement of "working in the same way for all types" can be formulated more rigorously: the code can only use a small number of constructions, but may have no side effects, no fixed values of fixed types, no run-time type information, and no calls to external libraries.
For code of that kind, the parametricity theorems, the Yoneda lemma, and the Curry-Howard correspondence hold and can be used for reasoning about the universally quantified types. In many cases, a universally quantified type may be simplified into a type that has no quantifiers.
Here are some examples of simplifying types:
∀A. A = 0 (the void type)
∀A. A → A = 1 (the unit type)
∀A. F(A) = F(0) if F is a covariant functor and F(1) if F is a contravariant functor.
∀A. (R → A) → A -- equivalent to R (here R is a fixed type, i.e., a free type variable)
All these examples follow from the Yoneda lemma.
∀A. (A → A) → (A → A) is equivalent to Church-encoded natural numbers.
This follows from the general theorem:
∀A. (F(A) → A) → A is the least fixed point of F if F is a covariant functor.
My main interest is to discover the techniques required for reasoning about those types and for simplifying to types without quantifiers. Most practically relevant examples can be solved with the Yoneda lemma. Recently I've been working on examples where the Yoneda lemma does not apply. Here are other techniques I found so far.
1) ∀A. F(A) = 0 when F(0) = 0
2) ∀A. F(A) × G(A) = (∀A. F(A) ) × (∀B. G(B) )
3) ∀A. F(A) + G(A) = (∀A. F(A) ) + (∀B. G(B) )
4) For a certain class of F(A) we have ∀A. F(A) → G(A) + H(A) = (∀A. F(A) → G(A) ) + (∀B. F(B) → H(B) )
5) For a certain class of F(A) we have ∀A. F(A) → G(A) = G(0) if G is a covariant functor.
6) For a certain class of F(A) we have ∀A. F(A) → P = P if P is a fixed type. This is proved via the relational parametricity theorem.
7) For a certain class of F(A) we have ∀A. (F(A) → P) → Q = P → Q if P, Q are fixed types. This is proved via the relational parametricity theorem.
8) If F(A) has no fixed types then ∀A. F(A) can be sometimes solved via the Curry-Howard correspondence. Each inequivalent proof of the constructive-logical formula ∀A. F(A) corresponds to a distinct value of type ∀A. F(A). If there is no proof, ∀A. F(A) = 0, and if there is only one proof, ∀A. F(A) = 1.
More examples where these techniques are used: (here P, R, etc. are fixed, given types, i.e., free type variables)
T1 = ∀A. (A → R) × A = 0 -- Techniques 1 and 2
T2 = ∀A. (A → A) → F(A) = F(0) if F is a covariant functor -- Technique 5
T3 = ∀A. (A → A) → R = R -- Technique 6
T4 = ∀A. (A → R) → A = 0 -- Yoneda
T5 = ∀A. ((A → R) → A) → R = R -- Yoneda
T6 = ∀A. ((A → R) → A) → A = ??? Nothing works so far.
T7 = ∀A. ((A → A) → A) → A = 1 -- Curry-Howard correspondence gives 1 proof
T8 = ∀A. ((A → A) → R) → S = R → S -- Technique 7
T9 = ∀A. ((A → P) → Q) → ((A → R) → S) = ((R → P) → Q) → S -- Yoneda
T10 = ∀A. (((A → P) → Q) → R) → (((A → S) → T) → U) = ??? Nothing works so far.
T11 = ∀A. (R → 1 + A) → 1 + A = ??? Nothing works so far.
T12 = ∀A. ((A → A) → A) → R = R -- Technique 6
The techniques for reasoning about those types are not simple but also not "deep" enough to be of interest to researchers. I'm still trying to figure out how to prove anything about the types I marked with "???".
def f[A]: (A, Option[A]) => Option[(A, A)] = {
case (x, oy) => oy.map(y => (x, y))
}
In a more mathematical type notation, the function f has type ∀A. A × (1 + A) → 1 + A × A.
The programmer's intuition for generic functions is that these functions work in the same way for all types. Indeed, the code of f does not depend on the type A and works in the same way for all A.
The requirement of "working in the same way for all types" can be formulated more rigorously: the code can only use a small number of constructions, but may have no side effects, no fixed values of fixed types, no run-time type information, and no calls to external libraries.
For code of that kind, the parametricity theorems, the Yoneda lemma, and the Curry-Howard correspondence hold and can be used for reasoning about the universally quantified types. In many cases, a universally quantified type may be simplified into a type that has no quantifiers.
Here are some examples of simplifying types:
∀A. A = 0 (the void type)
∀A. A → A = 1 (the unit type)
∀A. F(A) = F(0) if F is a covariant functor and F(1) if F is a contravariant functor.
∀A. (R → A) → A -- equivalent to R (here R is a fixed type, i.e., a free type variable)
All these examples follow from the Yoneda lemma.
∀A. (A → A) → (A → A) is equivalent to Church-encoded natural numbers.
This follows from the general theorem:
∀A. (F(A) → A) → A is the least fixed point of F if F is a covariant functor.
My main interest is to discover the techniques required for reasoning about those types and for simplifying to types without quantifiers. Most practically relevant examples can be solved with the Yoneda lemma. Recently I've been working on examples where the Yoneda lemma does not apply. Here are other techniques I found so far.
1) ∀A. F(A) = 0 when F(0) = 0
2) ∀A. F(A) × G(A) = (∀A. F(A) ) × (∀B. G(B) )
3) ∀A. F(A) + G(A) = (∀A. F(A) ) + (∀B. G(B) )
4) For a certain class of F(A) we have ∀A. F(A) → G(A) + H(A) = (∀A. F(A) → G(A) ) + (∀B. F(B) → H(B) )
5) For a certain class of F(A) we have ∀A. F(A) → G(A) = G(0) if G is a covariant functor.
6) For a certain class of F(A) we have ∀A. F(A) → P = P if P is a fixed type. This is proved via the relational parametricity theorem.
7) For a certain class of F(A) we have ∀A. (F(A) → P) → Q = P → Q if P, Q are fixed types. This is proved via the relational parametricity theorem.
8) If F(A) has no fixed types then ∀A. F(A) can be sometimes solved via the Curry-Howard correspondence. Each inequivalent proof of the constructive-logical formula ∀A. F(A) corresponds to a distinct value of type ∀A. F(A). If there is no proof, ∀A. F(A) = 0, and if there is only one proof, ∀A. F(A) = 1.
More examples where these techniques are used: (here P, R, etc. are fixed, given types, i.e., free type variables)
T1 = ∀A. (A → R) × A = 0 -- Techniques 1 and 2
T2 = ∀A. (A → A) → F(A) = F(0) if F is a covariant functor -- Technique 5
T3 = ∀A. (A → A) → R = R -- Technique 6
T4 = ∀A. (A → R) → A = 0 -- Yoneda
T5 = ∀A. ((A → R) → A) → R = R -- Yoneda
T6 = ∀A. ((A → R) → A) → A = ??? Nothing works so far.
T7 = ∀A. ((A → A) → A) → A = 1 -- Curry-Howard correspondence gives 1 proof
T8 = ∀A. ((A → A) → R) → S = R → S -- Technique 7
T9 = ∀A. ((A → P) → Q) → ((A → R) → S) = ((R → P) → Q) → S -- Yoneda
T10 = ∀A. (((A → P) → Q) → R) → (((A → S) → T) → U) = ??? Nothing works so far.
T11 = ∀A. (R → 1 + A) → 1 + A = ??? Nothing works so far.
T12 = ∀A. ((A → A) → A) → R = R -- Technique 6
The techniques for reasoning about those types are not simple but also not "deep" enough to be of interest to researchers. I'm still trying to figure out how to prove anything about the types I marked with "???".
no subject
Date: 2022-11-19 05:33 pm (UTC)This is beautiful. And a great idea in general, to dive into details.
no subject
Date: 2022-11-19 06:08 pm (UTC)https://en.cppreference.com/w/cpp/language/adl
no subject
Date: 2022-11-19 08:03 pm (UTC)Eh?... how come?
no subject
Date: 2022-11-19 08:10 pm (UTC)∀ A. X is really (A : Type) → X
So ∀A. F(A) × G(A) = (∀A. F(A) ) × (∀B. G(B) ) is really
(A: Type) → F(A) × G(A) = ((A: Type) → F(A) ) × ((B: Type) → G(B) )
Which is obviously true.
no subject
Date: 2022-11-21 06:57 am (UTC)This is more apparent with (2). What you mean there, is not (A : Set) → Either (F A) (G A), but (A : Set) → Set, whose implementation is λ A → Either (F A) (G A). Note the whole thing ((A : Set) → Set) is in Set 1, but its Either combines two types from Set 0.
Now, look what's on the right of the claimed equality. On the right you have a totally different universe, Set 2, because its Either combines types from Set 1.
(I am not an expert, so maybe I got the indices of the universes wrong, but they definitely are different universes)
no subject
Date: 2022-11-21 09:38 am (UTC)My criterion of correctness is having a working program code. If a function can be implemented and the compilers of ML, Haskell, Scala, etc. will accept it, then the concepts are correct and adequately express the reality of programming.
In all cases shown in my post, one can write a corresponding code in pretty much any FP language.
no subject
Date: 2022-11-21 10:08 am (UTC)∀A.X has the same problems as dependent types. Are you allowed to get a type that includes itself?
Something along these lines:
Suppose Y=∀A.X. doesn't it mean that X exists for Y as well, since Y is a type? Doesn't that mean X proves itself?
no subject
Date: 2022-11-21 11:28 am (UTC)Yes, Y = ∀A.X must be a type that works also for A = Y.
I don't think there are problems due to Y "proving itself". But there are no nice set-theoretic models for this.
Consider as an example a value of type ∀A. A × A → A, there are 2 distinct values of that type.
pi_1 : ∀A. A × A → A
pi_1 [A] (a1, a2) = a1
pi_2 : ∀A. A × A → A
pi_2 [A] (a1, a2) = a2
In Scala:
def pi_1[A](a1: A, a2: A): A = a1
def pi_2[A](a1: A, a2: A): A = a2
The functions pi_1, pi_2 work also for type A = ∀T. T × T → T because these functions work in the same way for all types.
no subject
Date: 2022-11-21 03:28 pm (UTC)Well, the problem is that it allows to populate any type, once you add polymorphism. But you want to consider a subset that doesn't allow this.
The way this is solved is by adding a so-called tower of universes. Then you can include Y "in X" - but that X is on the next universe from Y.
Also, really there is no difference between how you "simplify" F(A)×G(A) and F(A)+G(A). Why? Because it actually holds for any type of next universe (_×_ and _+_ are just examples, but the same can be done to _→_) of any arity. Since there really is no equality, the correspondence is arbitrary.
no subject
Date: 2022-11-21 05:05 pm (UTC)trait L[F[_]] { def run[A]: F[A] } // L is the type costructor for ∀A. F[A] def f[F[_], G[_], A]: Either[L[F], L[G]] => Either[F[A], G[A]] = { case Left(lf) => Left(lf.run[A]) case Right(lg) => Right(lg.run[A]) }This function type-checks and works. So, there is no mismatch between the universes or anything like that.
We can use the kind-projector syntax to make the type signature more uniform and to have the quantifier inside the function return type:
def f[F[_], G[_]]: Either[L[F], L[G]] => L[ ({ type H[A] = Either[F[A], G[A]] })#H ] = { case Left(lf) => new L[({ type H[A] = Either[F[A], G[A]] })#H ] { def run[X] = Left(lf.run[X]) } case Right(lg) => new L[({ type H[A] = Either[F[A], G[A]] })#H ] { def run[X] = Right(lg.run[X]) } }There is, unfortunately, no way of defining the inverse function in Scala because its existence depends on parametricity.
But there is no particular difficulty for the product:
def f[F[_], G[_], A]: (L[F], L[G]) => (F[A], G[A]) = { (lf, lg) => (lf.run[A], lg.run[A]) } def g[F[_], G[_]] : L[ ({ type H[A] = (F[A], G[A]) })#H ] => (L[F], L[G]) = lh => ( new L[F] { def run[A] = lh.run[A]._1 }, new L[G] { def run[A] = lh.run[A]._2 } )no subject
Date: 2022-11-21 06:46 pm (UTC)Your Scala example is not the function that we need. There is an implied argument, hidden as run: F[A] method.
Your Scala example does not (and I believe cannot) show equality, because the size of types is different. I.e. f . g /= id.
You don't need to automatically define the inverse. Just show that there exist such f and g that f . g == id, and that g . f == id. Then the types are equal (in the sense defined by HoTT; if that's not suitable, you need to define your own equality and everything that comes with it).
no subject
Date: 2022-11-21 03:38 pm (UTC)No, no, no. You are confusing the level where you are working with the type.
Try to do the same to F(A)+G(A), which gets translated into F+G. If you think about it as a value, then it has either F, or G, but not both.
The only level where (2) can even be discussed, is really type construction. That is, a type (A : Set) → F(A)+0G(A) vs type ((A : Set) → F(A))+1((B : Set) → G(B)) = F+1G. I am not sure how to even begin to express something like an equivalence - how to capture the existence of an isomorphism.
no subject
Date: 2022-11-21 04:24 pm (UTC)Let's see what functions we are talking about.
f : (F G : (A : Set)) → (F + G) → (A : Set) → (F A) + (G A) f F G (Left .F) = λ A → Left {! What goes here? !} ... --- ditto for Right G -- similar for g working the other way.I have a problem filling in the hole. It must have a way of constructing a value of an arbitrary type F(_), which includes the type λ_ → ⊥.
A problem with g is even worse. It should map any value of type λ A → F(A)+G(A). But there is just one such value (not proven either) for two values of type F+G.
no subject
Date: 2022-11-21 05:08 pm (UTC)No, I'm not confusing anything. I am asking the question about how to inhabit the type ∀A. A × A → A and I am giving two inhabitants.
> F(A)+G(A), which gets translated into F+G.
I don't agree with that. Nothing gets translated into F+G. I am asking the question about how to inhabit the type ∀A. F(A)+G(A) by terms of the polymorphic lambda calculus. The answer is, you have to give either a value of type ∀A. F(A) or a value of type ∀A. G(A) because the polymorphic lambda calculus satisfies parametricity and there is no way to make a decision about left and right based on the type of A.
no subject
Date: 2022-11-21 07:06 pm (UTC)First consider what a polymorphic term is. Let's say, write a function f :: ()->forall a.(a,()). In Haskell this amounts to a bottom. Because that's the only way to construct a term that can be any type.
In essence, a function doesn't know the context, but the return value will fit any context.
no subject
Date: 2022-11-21 07:42 pm (UTC)It is exactly that translation. I wrote the Scala code that maps from a value of type ∀A.F(A)+G(A) to a value of type (∀A.F(A))+(∀A.G(A)). The trait L[F] represents the type ∀A.F(A) because in Scala 2 we can't have a type lambda or a polymorphic value. In Scala 3 the syntax will be somewhat shorter.
Where is the error, in your opinion?
I don't see the point in your explanations.
> Let's say, write a function f :: ()->forall a.(a,()).
Let's not write that function, because it's not relevant to what we are discussing.
You are repeating the first example in my post: ∀A.A = 0 . I don't see how that example is relevant to discussing ∀A.F(A)+G(A).
no subject
Date: 2022-11-21 11:39 pm (UTC)The error is in the wrong level where you make assertions. The error is in the rejection of the truth that ∀A.X in polymorphic lambda is nothing but a function (A : Type)→X. This last one is actually quite strange, since that's exactly the definition of a function in FP.
> I wrote the Scala code that maps from a value of type ∀A.F(A)+G(A) to a value of type (∀A.F(A))+(∀A.G(A)).
No, you wrote code that translates values of type F(A)+G(A) for a given A. The subtle difference becomes apparent once you accept that ∀A.X in polymorphic lambda is nothing but a function (A : Type)→X.
The value of type ∀A.F(A)+G(A) is not Either, but a function that gets you Either F(A) G(A), if you pass it a type.
no subject
Date: 2022-11-22 10:22 am (UTC)But of course I accept it. That's how I write all the code examples. It is a function from type to a value. In Scala, the type argument is written in square brackets.
A function (A : Type)→X is written in Scala as "def f[A]: X = ..."
> you wrote code that translates values of type F(A)+G(A) for a given A.
No, actually I did not write any such code.
In my comment above, I wrote a Scala function between (∀A. F(A) ) + (∀B. G(B) ) and ∀A. F(A) + G(A). Not in the opposite direction! And I added a comment that it's not possible to write an explicit Scala function in the opposite direction (even though that function exists once we impose parametricity).
But then I pasted the wrong type signature into my previous comment:
> I wrote the Scala code that maps from a value of type ∀A.F(A)+G(A) to a value of type (∀A.F(A))+(∀A.G(A)).
This should have been written like this:
> I wrote the Scala code that maps from a value of type (∀A.F(A))+(∀A.G(A)) to a value of type ∀A.F(A)+G(A).
The Scala code I wrote had that type signature.
There is no error about the "level of universes" anywhere. Please point out where I have mixed up any "universes" and what would be the correct Scala code.
no subject
Date: 2022-11-22 10:43 am (UTC)Two problems with this :)
1. Scala is not exactly consistent - you are allowed to populate type 0
2. How can I write correct code for the thing that I claim should not be possible?
> ∀A. F(A)+∀A. G(A) vs ∀A. (F(A) + G(A))
Ok, let's drop for now the question of the direction. I may have gotten confused. My problem is in a different place anyway.
So, you do say ∀A.A=0. Let's start with your explanation of what makes ∀A. F(A) different _for_ _all_ F.
I insist on you writing a function ()->forall a.F(a), not just forall a.F(a), because we can agree that X and ()->X are isomorphic, but writing a function will expose what is wrong with the claim that you wrote a function transforming forall a.F(a), not a function for transforming F(a) for a given a. (To me it is so obvious - the body of a function is always for a given argument - in this case a type)
The next step is to transform ()->forall a.F(a) into a desired type, not forall a.F(a). Again, they are isomorphic, right?
no subject
Date: 2022-11-22 01:07 pm (UTC)As I already said, I'm working with a lambda calculus, or pure subset of Scala or Haskell that does not allow us to inhabit 0.
Do you mean that my code example is an example of Scala code that inhabits 0? How does it do that, where is the deviation from lambda calculus?
> 2. How can I write correct code for the thing that I claim should not be possible?
I am asking you either to point out the error in my Scala code, or to write a different Scala code, or to show that it is not possible to transform a value of type (∀A.F(A))+(∀A.G(A)) to a value of type ∀A.F(A)+G(A).
My code, especially in its second form, is not a function for transforming F(a) for a given a. It is explicitly a function from Either[L[F], L[G]] to Either[L[F+G]].
But even in the first form, the code is correct because of the following type equivalence:
∀A. P → G(A) = P → ∀A. G(A) as long as P does not depend on A.
> I insist on you writing a function ()->forall a.F(a)
Are you talking about the definition of the trait L? Would you like to define a different type L2 as follows:
trait L[F[_]] { def run[A]: F[A] } // L is the type costructor for ∀A. F[A]
type L2[F[_]] = () => L[F] // L2 is the type costructor for 1 → ∀A. F[A]
Now we can easily rewrite my code example using L2 instead of L.
def f[F[_], G[_]]: Either[L2[F], L2[G]] => L2[ ({ type H[A] = Either[F[A], G[A]] })#H ] = {
case Left(lf) => () => new L[({ type H[A] = Either[F[A], G[A]] })#H ] { def run[X] = Left(lf().run[X]) }
case Right(lg) => () => new L[({ type H[A] = Either[F[A], G[A]] })#H ] { def run[X] = Right(lg().run[X]) }
}
There are no problems with any "universes" anywhere.
no subject
Date: 2022-11-22 02:08 pm (UTC)You saying so doesn't make it so :)
You've discarded the idea of the towers of universes, and allowed to include the type in itself. Isn't this how one might populate an empty type?
> .run
I've explained that in presence of invocation of _methods_ you are no longer dealing with the types you declared - you can no longer treat Scala types as direct translation of lambda. There is an implicit argument that we could call "a dictionary of functions". Suddenly it is no longer a proof of equality of types.