I'm a bit more interested in what it teaches about the hyperbolic plane than I am in it's effectiveness as a note taking app (although the way it supports an exponentially growing tree does seem appropriate for depicting knowledge - I'd be interested to see something like a force directed graph of Wikipedia plotted on the hyperbolic plane).
The points and arrows do move and change shape appropriately while panning, but the images and text do not. It might be possible to use feDisplacementMap (an SVG filter effect) cleverly to get the deformations right. This would probably make performance worse, and I'm not sure how readable the text would be, but it would mean that things wouldn't start overlapping each other while panning.
> As seen after the Black Death, a scarcity of labor drives real wages up and lower the cost of basic goods and rent.
Does this still hold when the majority of labor is no longer closely tied to a finite supply of land? At the time of the Black Death, the majority of men's labor was farming, and having more land directly made labor much more productive[1]. The modern economy feels much more complicated (e.g. if your job involves transporting things/people from A to B, it probably decreases in efficiency as the density of people decreases).
I'm open to the possibilty of AI conciousness, and there is some desparation related to the concept of a higher being:
There are many people who will categorically rule out the posibility of AI consciousness due to near-unshakable belief in a higher being. This argument resembles "Christians should not be worried about our climate since God is ultimately in control." Such views make it harder to collectively prevent dangers from a sentient AI, or harm to a sentient AI.
I do not claim that everyone who believes in a higher power believes concious AI to be impossible, or vice versa; just that it would be very hard to change the minds of those who adhere to this reasoning.
Very cool. I was expecting it to make circles bigger rather than making needles smaller. Take a near-circle consisting of N lines. As N tends to infinity, the near-circle would have a diameter close to N*L/π, so would touch N*L/πW + O(1) lines twice each.
Many people move to London when they want to make money, and move out when they want to do anything else. Pretending that London is independent of the rest of the country's children and retirees is misleading.
No idea if they are doing this, but you can use Gosper islands (https://en.wikipedia.org/wiki/Gosper_curve) which are close to hexagons, but can be exactly decomposed into 7 smaller copies.
Yes! A Gosper Island in H3 is just the outline of all the descendants of a cell at a some resolution. The H3 cells at that resolution tile the sphere, and the Gosper Islands are just non-overlapping subsets of those cells, which means they tile the sphere.
Not quite - you need 12 pentagons in a mostly hexagonal tiling of the sphere (and if you're keeping them similar sizes, Gosper-islands force hexagon-like adjacency). I don't think it's possible to tile the sphere using more than 20 exactly identical pieces.
You could get a Gosper-island like tiling starting from H3 by saying that each "Hex" is defined recursively to be the union of its 6/7 parts (stopping at some small enough hexagons/pentagons if you really want). Away from the pentagons, these tiles would be very close to Gosper islands.
> I don't think it's possible to tile the sphere using more than 20 exactly identical pieces.
I was wrong about this (e.g. https://en.wikipedia.org/wiki/Rhombic_triacontahedron). It still seems possible to me that there's a limit to the smallest tile that can tile a unit sphere on its own. (Smallest by diameter as a set of points in R^3).
Decidability of a type system is like well-typedness of a program. It doesn't guarantee it's sensible, but not having the property is an indicator of problems.
I'm not entirely smart enough to connect all of these things together but I think there is a kind of subtlety here thats being stepped on.
1. Complete, Decidable, Well founded are all distinct things.
2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter.
3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox.
4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation.
6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway....
Your other points are more relevant to the content of the article, but point 2. relates the practical consequences of undecidable type-checking, so I'll reply to that.
I don't have a problem with compile time code execution potentially not terminating, since it's clear to the programmer why that may happen. However, conventional type checking/inference is more like solving a system of constraints, and the programmer should understand what the constraints mean, but not need to know how the constraint solver (type checker) operates. If it's undecidable, that means there is a program that a programmer knows should type check, but the implementation won't be happy with; ruining the programmer's blissful ignorance of the internals.
> 2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter.
Being Turing complete at compile time causes the same kinds of problems as undecidable typechecking, sure. That doesn't make either of those things a good idea.
> 3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox.
A set that violates an axiom is immediately a paradox from which you can prove anything. See the principle of explosion.
> 4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation.
Well, sure, that's what a set is. I don't think it's weird; quite the opposite,
> 5. This isn't nessesarily some axiomatically self evident fact. Aczel's anti foundation axiom works as well and you can make arbitrary sets with weird memberships if you adopt that.
I don't think this kind of thing is established enough to say that it works well. There aren't enough people working on those non-standard axioms and theories to conclude that they're practical or meet our intuitions.
> 6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway....
The Axiom of Foundation exists to make induction work, and so does the Axiom of Choice. They both express a sense that if you can start and you can always make progress, eventually you can finish. It's very hard to prove general results without them.
But like, of all the
expressive power vs analyzability
trade-offs you can make,
there's a huge leap in expressive power
when you give away decidability.
Undecidability is not a sign
that the foundation has cracks
(not well founded),
but it might be a sign
that you put the foundation on wheels
so you can drive it at highway speeds,
with all the dangers that entails.
It's not a trade everyone would make,
but the languages I prefer do.
No. Being well typed is not a semantic property of of a program - in a language where it makes sense to talk about running badly typed code, a piece of code that starts with an infinite loop may be well or badly typed after that point with no observable difference in program behaviour.
There are decidable type systems for Turing complete languages (many try to have this property), and there are languages in which all well typed programs terminate for which type checking is undecidable (System F without all type annotations).
reply