TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

Monotonicity Types: Towards a Type System for Eventual Consistency

101 点作者 cmeiklejohn超过 7 年前

4 条评论

warent超过 7 年前
For anybody looking for additional footing on understanding this, I found the following to be very helpful: <a href="http:&#x2F;&#x2F;bloom-lang.net&#x2F;calm&#x2F;" rel="nofollow">http:&#x2F;&#x2F;bloom-lang.net&#x2F;calm&#x2F;</a><p>Personally, I&#x27;ve never done programming on distributed systems before so please correct me if I&#x27;m off at any point. The issue seems quite clear: you want to ensure that your function mutates inputs (or returns values relative to inputs) in a predictable way with values headed in one direction--increasing or decreasing. So, the idea of monotonicity types actually seems quite intuitive: ensure your outputs monotonicity are well-defined. It&#x27;s mildly surprising this isn&#x27;t something that has already been implemented.<p>On the other hand, could this monotonic type could be more generalized? Maybe something less two-dimensional, though perhaps this is overkill for most uses.<p>Also, as an aside, I don&#x27;t have a Ph.D. in comp. sci, type theory, mathematics, or anything for that matter. This article was borderline gobbledygook to me and could be summarized far more succinctly (in a manner more friendly to the general programming public?)
fmap超过 7 年前
Great work and obscure enough that I&#x27;m sure one of the authors made the submission :)<p>If so, here are a few things that I saw while glancing over the paper (I&#x27;ll read the paper in detail later):<p>- you might be interested in neel krishnaswami&#x27;s paper on datafun, which is a functional language that includes datalog primitives in the form of least fixed points of monotone functions. Monotonicity is tracked in the type system, so this seems very relevant.<p>Edit: just saw that the paper was referenced after all, my bad!<p>- why do you need termination? Is it an artifact of the logical relation you use? If so, step indexing might help to relax this restriction.
评论 #15728532 未加载
doomrobo超过 7 年前
Could anyone provide some intuition for what&#x27;s supposed to be happening in the sample code?
评论 #15727759 未加载
auggierose超过 7 年前
Great. 35 points and no discussion. I’d say that tells you SOMETHING about type theory.
评论 #15727777 未加载