I keep trying to get the gist of type theory and it's like eating unflavored jello.
-
Show this thread
-
-
Replying to @Meaningness
The treatments I've seen just talk in circles around the subject without getting down to anything concrete. And no results! Just handwaving.
1 reply 0 retweets 3 likes -
Replying to @St_Rev @Meaningness
"we replace homotopy, which is a fairly delicate mathematical construction whose existence has to be checked and proven, with...a colon, which just sits there and magically does the same thing"
1 reply 0 retweets 3 likes -
Replying to @St_Rev
In practice the point seems to be that it provides a notation for expressing simple properties of programs like "returns a vector of positive integers."
2 replies 0 retweets 2 likes -
Replying to @Meaningness @St_Rev
From contexdt, I think
@st_rev is talking specifically about homotopy type theory. I also don't know if there's a there there, but it's shiny. I seem to remember it at least motivated a new proof of a classic result, but I can't find it...2 replies 0 retweets 1 like -
Replying to @postreptilian @St_Rev
Yeah I dunno, there’s so much excitement about it that once every few months I feel like I ought to figure out what it’s about, but every time I spend half an hour looking at it, it seems highly unpromising and I set it aside again.
1 reply 0 retweets 1 like -
E.g. it’s hard for me to imagine how homotopy, which is about continuous deformations of continuous functions, could give leverage in ToC, where nothing is continuous. Presumably I’m missing something because I haven’t even bothered to look this up, but
2 replies 0 retweets 0 likes -
To make an analogy: Euclid's Axioms :: Real Cartesian Plane as Homotopy Type Theory :: Spaces of various sorts. We work up to homotopy equivalence, so all the data you care about can be presented combinatorially...
1 reply 0 retweets 0 likes -
Replying to @11kilobytes @Meaningness and
e.g. the HoTT "circle" is freely generated by a point and a primitive-axiomatic path between that point and itself. This _means_, e.g. that to map it somewhere else is to give a loop there.
2 replies 0 retweets 0 likes
I’m sorry, without reading up on a bunch of definitions, I don’t know what that means. How does homotopy apply to computation, in which all the “spaces” are at-most-countable sets of discrete objects? What is the topology?
-
-
Here's an analogy that might help: HoTT is to topology as Euclid's axioms are to the real coordinate plane. In Euclid's axioms we talk about points, by saying what you can do with them (construct lines, circles, intersections, etc.) instead of talking about the reals at all.
1 reply 0 retweets 0 likes -
Replying to @11kilobytes @Meaningness and
Similarly in HoTT we have a primitive Paths-Between(x, y) type for any x, y in a type A. It is primarily defined by the axiom that if you want to define something for arbitrary paths with unconstrained endpoints, you can assume that you are dealing with a constant path.
1 reply 0 retweets 0 likes - 5 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.