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
It seems like a ridiculous amount of machinery for that purpose, though. Particularly as a main motivation for type theory and category theory was to deal with things that are too big to be sets, whereas everything in computation is at most countably infinite.
1 reply 0 retweets 3 likes -
Replying to @Meaningness @St_Rev
I haven't bothered to work through the details, but my working assumption assume if you assume countability it collapses into mathematically trivial (which is why there are no results). It's just notation.
1 reply 0 retweets 3 likes
I am reminded of @dannyhillis's satire "Dynamics of Manipulators with Less Than One Degree of Freedom":
https://dspace.mit.edu/handle/1721.1/41188 …
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.