Paul Cantrell@jrose I think part of the long-term appeal of dependent types is their Golden Hammer promise that this family of tradeoffs doesn’t have to exist, that this horizon can extend to infinity. I’m…skeptical. Good and fascinating things there, but I’m not going to bet in favor of that grandiose promise.
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.