Reason Isomorphically!
May. 11th, 2020 10:12 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
xacidhttp://www.cs.ox.ac.uk/people/daniel.james/iso/iso.pdf
When are two types the same? In this paper we argue that isomorphism is a more useful notion than equality. We explain a succinct and elegant approach to establishing isomorphisms, with our focus on showing their existence over deriving the witnesses. We use category theory as a framework, but rather than chasing diagrams or arguing with arrows, we present our proofs in a calculational style. In particular, we hope to showcase to the reader why the Yoneda lemma and adjunctions should be in their reasoning toolbox.
When are two types the same? In this paper we argue that isomorphism is a more useful notion than equality. We explain a succinct and elegant approach to establishing isomorphisms, with our focus on showing their existence over deriving the witnesses. We use category theory as a framework, but rather than chasing diagrams or arguing with arrows, we present our proofs in a calculational style. In particular, we hope to showcase to the reader why the Yoneda lemma and adjunctions should be in their reasoning toolbox.
no subject
Date: 2020-05-11 09:17 pm (UTC)no subject
Date: 2020-05-12 06:14 am (UTC)http://people.math.harvard.edu/~mazur/preprints/when_is_one.pdf
no subject
Date: 2020-05-12 01:51 am (UTC)Впрочем, как писал Бауэр, Хаск и не категория вовсе, а так.
no subject
Date: 2020-05-12 06:12 am (UTC)а еще там вот что пишут (просто понравилось):
Central to the latter undertaking is the Yoneda lemma, which
support an indirect mode of reasoning. Because of its central importance
it also appears in every textbook on category theory, [5, 16]
being no exceptions. Unfortunately, often only the abstract result is
presented, leaving readers unenlightened and depriving them of a
powerful reasoning tool. We have hinted at another link to computing
science: continuation-passing style.
no subject
Date: 2020-05-12 01:52 pm (UTC)no subject
Date: 2020-05-12 02:14 pm (UTC)A set-valued functor H:C -> Set is representable if there exists a rep
resenting object X:C such that C(X, - ) ~= H
An object X is the coproduct of A1 and A2 if it solves the equation
C(X, -) ~= C(A1, -) x C(A2,-)
The equation between functors demands that a pair of functions to a common targe
t can be represented by a single function from X to the target, and vice versa.
We write X as A1 + A2. This is a representational approach to defining co
products, where we define an object in terms of a representation rather than its
construction.
это из статьи по ссылке если что) выглядит вроде понятно даже мне
no subject
Date: 2020-05-12 02:06 pm (UTC)no subject
Date: 2020-05-12 02:18 pm (UTC)no subject
Date: 2020-05-12 03:18 pm (UTC)no subject
Date: 2020-05-12 03:50 pm (UTC)я так понимаю что скелет это уже типа результат (тоже категория?) типа как диаграмма
а какой функтор или там еще как это мы сделали - вопрос отдельный?
no subject
Date: 2020-05-12 05:33 pm (UTC)Why not? Just not a faithful functor. (Surjective)
> а как функтор вычисляет изоморфность обьектов?
No need. What you need, is map arrows that are isomorphisms into id of some object. Then a functor is bound to map the objects on both ends of isomorphism into the same object to preserve composition.
no subject
Date: 2020-05-12 05:17 pm (UTC)I know it's the famous Yoneda Lemma, but in this light it looks strange.
I am still under impression that for inhabited types A type (A→⊥)→(A→⊥) is isomorphic to T because (A→⊥) cannot be inhabited, and (A→⊥)→(A→⊥) can only have one function, id, hence isomorphism to T.
If this is so, then how can A→A be isomorphic to (A→⊥)→(A→⊥)? But if it _is_ isomorphic, then how come (A→⊥)→(A→⊥) has more than one inhabitant?
no subject
Date: 2020-05-12 05:41 pm (UTC)could you show that?
no subject
Date: 2020-05-12 05:54 pm (UTC)I think I start to understand that my premise what polymorphic functions mean, is wrong. I used to imagine that ∀ X . A→X is a negation (I was told CPS is double-negation, that's why!), the same as A→⊥. But now I seem to get that it is not so. ∀ X means one more argument, and CPS is double negation only for X=⊥.
no subject
Date: 2020-05-13 06:43 am (UTC)https://www.researchgate.net/publication/329014677_Negating_as_turning_upside_down
Also for me personally, it seems like there are a lot of different negations in several (but not all) categories.
So, Curry-Howard isomorphism double negation interpretation (a →⊥)→⊥ ≃ 𝟭 not necessarily implies (a → 𝟬)→𝟬 ≃ a in 𝗦𝗲𝘁
no subject
Date: 2020-05-13 07:06 am (UTC)That is, for all a = b → ⊥ for some b.
no subject
Date: 2020-05-13 10:25 pm (UTC)So far I can only notice that such double negation is just some special case of CPS which is more general (a -> r) -> r
and, probably, as you already might noticed too, if negation is understood as functorial contravariance then we could say that general CPS functor is double negation as well, right?
which implications are following there is still the question :)
no subject
Date: 2020-05-14 07:08 am (UTC)Curry-Howard isomorphism establishes a correspondence between types and propositions, and proofs and programs.
That is, a proposition is true, if there is a program of the corresponding type. This means a type is inhabited.
A false is represented by a type postulated to be uninhabited, ⊥. (Notice "postulated" - this is the type whose emptiness does not require a proof)
A negation is represented as implication of false. You will recall this from the definition of implication.
That is, a proposition "not A" is a type A→⊥. You can easily see that for inhabited types A type A→⊥ is uninhabited, and for uninhabited types A type A→⊥ is inhabited. What is the latter one inhabited with? A function that establishes isomorphism of types A and ⊥ (or you could think of id⊥ in the skeleton category).
Then to see the former case, that A→⊥ is uninhabited for an inhabited type A, consider idA→⊥: (A→⊥)→(A→⊥). Given a witness of type A (given a proof that A is inhabited), (flip id) can produce a proof that (A→⊥) is isomorphic to ⊥ - i.e. A→((A→⊥)⊥). This is only one side of isomorphism.
The other part of isomorphism is always there: it is postulated that there is an arrow from uninhabited type ⊥ to every other type such that any diagrams with it commute. You can see this as the existence of ⊥→A - existence without a proof (because it is postulated). You can also see this as the part of implication where "everything follows from false premise - both false (id) and true".
The "any diagrams with it commute" means that ⊥→A≡B→A for any B, if B→A factors through ⊥ - that is, if at some point you are able to compute an "instance" of ⊥.
Now we can show that (B→⊥)→⊥≡B for B=A→⊥. You can see that this can be rewritten as ((A→⊥)→⊥)→⊥≡A→⊥, which is none other than a proof of extensional equality of two functions.
Extensional equality of functions f and g of type A→B is: given any value of type A they should produce equal values of type B. That is a proposition of type (a:A)→(f a≡g a). If this proposition is inhabited for given f and g, then we call type f≡g inhabited (equality of functions proven).
The proof is trivial:
flatten-triple : {A : Set} ((((A→⊥)→⊥)→⊥)) → (A→⊥)
flatten-triple f a = f (flip id a)
bool : {A : Set} (g : A→⊥) → flatten-triple (flip id g) ≡ g
bool g = ext λ a → ⊥-elim (g a) -- remember the function from ⊥ to any type? Here is the arrow to the type flatten-triple (flip id g) a ≡ g a
Then we use extentionality axiom to prove double negation of g and g are equal. Since we can do this for any witness g, we conclude the types are isomorphic: composition of (flip id) and flatten-triple is id; you can similarly show the opposite, too; two types have arrows whose composition is respective id - isomorphism established, and the types are proven equivalent (and equal, if we have univalence axiom).
If double negation of A is equal to A, the logic is boolean. So the whole negative segment of intuitionistic logic is boolean. (That is, the segment of types that are of the form A→⊥)
You can see why this is so. Remember that all types of the form A→⊥ are either empty (contain no functions; the type is isomorphic to ⊥) or contain one function, id (the type is isomorphic to T). This observation makes the negative segment so boring: it's all just ones or zeros!
no subject
Date: 2020-05-14 02:33 pm (UTC)I guess that it could be possible only in some special categories where exists a morphism call/cc:((α→β)→α)→α
https://en.wikipedia.org/wiki/Peirce%27s_law
also, in cartesian closed category, according to
https://ncatlab.org/nlab/show/dualizing+object+in+a+closed+category
Proposition 3.1. A cartesian closed category C that is self-dual (carries an equivalence N:C op →C) is necessarily a preorder (whose posetal reflection is then a Heyting algebra). If the self-duality comes from a dualizing object, then the Heyting algebra is a Boolean algebra.
no subject
Date: 2020-05-14 03:04 pm (UTC)The weird notation is:
C(A,B) ≅ ∀ X . C(B,X) → C(A,X)
The _→_ is not just a function from a set to a set here. What does ∀ X mean? They mean many more unsaid things. Because it really should be a Hom-set for a category of functors from C to Set - eg commutativity implied (for C(B,X)→C(A,X) and C(B,Y)→C(A,Y) for all functions f : X→Y).
no subject
Date: 2020-05-14 04:27 pm (UTC)There is an isomorphism between the types of fac, the factorial function in CPS style, and the direct factorial function of type Nat -> Nat. Applying the identity function is one direction of the isomorphism, from CPS to direct style.
The factorial isomorphism is an instance of the isomorphism of the types A -> B and
∀X : (B -> X) -> (A -> X).
The covariant homfunctor for a fixed object A is C(A, -) : C -> Set,
with the action on arrows given by C(A, f ) h = f . h
The functor C(A, -) maps an object B to the set of arrows from a fixed A to B,
and it takes an arrow f : C(X, Y ) to a function.
C(A, f ) : C(A, X) -> C(A, Y ).
Conversely, C(-. B) : C op -> Set is a covariant functor defined C(f, B) h = h . f
Let us continue by transliterating the CPS isomorphism into more categorical language,
C(A, B) = ∀X : C(B, X) -> C(A, X)
We can continue generalizing by extracting out the covariant homfunctor C(A, - ) and naming it H.
HB = ∀X : C(B, X) -> HX
The covariant hom-functor has type C -> Set, and in one final abstraction we can let H : C -> Set be any set-valued functor.
The isomorphism we have arrived at is a statement of the Yoneda lemma.
no subject
Date: 2020-05-15 10:13 am (UTC)> ∀X : C(B, X) -> C(A, X)
What's this in categorical language?
Suppose this is a set, because C(A,B) is a set. Does it describe a set of all functions between sets C(B,X) and C(A,X)? No, it should not, because X is not fixed.
Is this then a set of functions (X : Set) -> C(B, X) -> C(A, X)? That is, a function from a set of types (it is a set, because C is small) to a set of functions from C(B,X) to C(A,X)? No, Yoneda lemma specifically restricts this to such a set of functions that make things commute.
I know Yoneda lemma means Hom(C(B,_), C(A,_)) in this place. It is this fact that makes things commute in that notation - that is, the fact that this set is the set of arrows between functors in the category SetC.
Besides, this is exactly what they don't explain - how one jumps from parametricity to natural transformations. I know everyone does it, but this notation is hardly an explanation.
no subject
Date: 2020-05-15 10:54 pm (UTC)> What's this in categorical language?
Natural transformation
no subject
Date: 2020-05-14 07:53 am (UTC)no subject
Date: 2020-05-14 01:30 pm (UTC)https://hal.archives-ouvertes.fr/file/index/docid/339156/filename/linear-control.pdf
At the moment, I'm not sure ( I still not read whole the paper above, just begun), but I think that we could see it a such way:
It's well known that Hom-bifunctor [-,=] is contravariant on its first parameter and covariant in its second one. So, fixing the first parameter with some free X we have got a covariant functor [X,-], but if we're fixing the second parameter we have got a contravariant functor [-, Y].
Moreover, according to Yoneda lemma, we could define a natural isomorphism (adjointion) between these two functors. Natural isomorphism consists of two opposite directed polymorphic functions (natural transformations) which reverse each other one. Such way, we have got duality relation and therefore some kind of pure algebraic negation (like negative values in algebraic equations are arising from carrying across equality from right to left) in form of contravariance of hom-set functor [-,Y]. Composing this negative functor to itself we get double negation (and therefore covariant) in continuation functor of [[-,Y],Y]
More of it at
https://ncatlab.org/nlab/show/continuation+monad
https://ncatlab.org/nlab/show/dualizing+object+in+a+closed+category
no subject
Date: 2020-05-14 03:18 pm (UTC)ncatlab speaks of continuation monad working one way: A→(A→B)→B. That's not problematic. What I am curious about, is it working the opposite way - ((A→B)→B)→A. That would mean the logic of CCC is boolean. I did not think it was.
no subject
Date: 2020-05-14 04:06 pm (UTC)call/cc:((α→β)→α)→α
https://en.wikipedia.org/wiki/Call-with-current-continuation#Relation_to_non-constructive_logic
The Curry–Howard correspondence between proofs and programs relates call/cc to Peirce's law, which extends intuitionistic logic to non-constructive, classical logic: ((α → β) → α) → α. Here, ((α → β) → α) is the type of the function f, which can either return a value of type α directly or apply an argument to the continuation of type (α → β). Since the existing context is deleted when the continuation is applied, the type β is never used and may be taken to be ⊥, the empty type.
The principle of double negation elimination ((α → ⊥) → ⊥) → α is comparable to a variant of call-cc which expects its argument f to always evaluate the current continuation without normally returning a value. Embeddings of classical logic into intuitionistic logic are related to continuation passing style translation.[4]
no subject
Date: 2020-05-14 05:44 pm (UTC)((α → β) → α) → α is not problematic. ((α → β) → α) → α comparison to ((α → ⊥) → ⊥) → α is problematic. For example, where will call-cc get α from? How do they get call-cc return type is α? Why is it not ((α → ⊥) → ⊥) → ⊥? (Not problematic again)
no subject
Date: 2020-05-15 10:19 pm (UTC)p.130 Chapter 8. Classical logic and control operators
"Another possibility is to add Peirce’s law in the form
((φ → ψ) → φ) → φ,
together with ex-falso in the form ⊥ → φ."
Provided with ((α → β) → α) → α you can set β = ⊥ and get (¬α → α) → α
which you can reduce by contradiction with absurd:⊥ → α to get ¬¬α → α
https://xacid.dreamwidth.org/93928.html
no subject
Date: 2020-05-15 11:31 pm (UTC)Say, in Haskell ignoring β does not imply that it is ⊥ - it is kept for side-effects.
no subject
Date: 2020-05-16 12:34 am (UTC)For side effects one typically uses unit type ()
no subject
Date: 2020-05-16 07:17 am (UTC)It doesn't matter whether you are going to get α from ¬¬α after that: you simply end up with a broken logic.
In Haskell call-cc is in ContT, and the type is ((a->m b)->m a)->m a for some monad m. Replacing m b with ⊥ would be very brave. (And it's obvious the function that receives m b can only use the result for side-effects, whatever they may be in monad m.)