اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدUnifying graded and parameterised monads
336
0
0.0
(
0
)
تأليف
Dominic Orchard
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Monads are a useful tool for structuring effectful features of computation such as state, non-determinism, and continuations. In the last decade, several generalisations of monads have been suggested which provide a more fine-grained model of effects by replacing the single type constructor of a monad with an indexed family of constructors. Most notably, graded monads (indexed by a monoid) model effect systems and parameterised monads (indexed by pairs of pre- and post-conditions) model program logics. This paper studies the relationship between these two generalisations of monads via a third generalisation. This third generalisation, which we call category-graded monads, arises by generalising a view of monads as a particular special case of lax functors. A category-graded monad provides a family of functors T f indexed by morphisms f of some other category. This allows certain compositions of effects to be ruled out (in the style of a program logic) as well as an abstract description of effects (in the style of an effect system). Using this as a basis, we show how graded and parameterised monads can be unified, studying their similarities and differences along the way.
قيم البحث
اقرأ أيضاً
Given an operad A of topological spaces, we consider A-monads in a topological category C . When A is an A-infinity-operad, any A-monad K : C -> C can be thought of as a monad up to coherent homotopies. We define the completion functor with respect t
o an A-infinity-monad and prove that it is an A-infinity-monad itself.
This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, th
us covering new applications such as lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. Moreover, we design a suitable notion of signature for transition monads.
We reflect on programming with complicated effects, recalling an undeservingly forgotten alternative to monadic programming and checking to see how well it can actually work in modern functional languages. We adopt and argue the position of factoring
an effectful program into a first-order effectful DSL with a rich, higher-order macro system. Not all programs can be thus factored. Although the approach is not general-purpose, it does admit interesting programs. The effectful DSL is likewise rather problem-specific and lacks general-purpose monadic composition, or even functions. On the upside, it expresses the problem elegantly, is simple to implement and reason about, and lends itself to non-standard interpretations such as code generation (compilation) and abstract interpretation. A specialized DSL is liable to be frequently extended; the experience with the tagless-final style of DSL embedding shown that the DSL evolution can be made painless, with the maximum code reuse. We illustrate the argument on a simple but representative example of a rather complicated effect -- non-determinism, including committed choice. Unexpectedly, it turns out we can write interesting non-deterministic programs in an ML-like language just as naturally and elegantly as in the functional-logic language Curry -- and not only run them but also statically analyze, optimize and compile. The richness of the Meta Language does, in reality, compensate for the simplicity of the effectful DSL. The key idea goes back to the origins of ML as the Meta Language for the Edinburgh LCF theorem prover. Instead of using ML to build theorems, we now build (DSL) programs.
We present a unification of refinement and Hoare-style reasoning in a foundational mechanized higher-order distributed separation logic. This unification enables us to prove formally in the Coq proof assistant that concrete implementations of challen
ging distributed systems refine more abstract models and to combine refinement-style reasoning with Hoare-style program verification. We use our logic to prove correctness of concrete implementations of two-phase commit and single-decree Paxos by showing that they refine their abstract TLA+ specifications. We further use our notion of refinement to transfer fairness assumptions on program executions to model traces and then transfer liveness properties of fair model traces back to program executions, which enables us to prove liveness properties such as strong eventual consistency of a concrete implementation of a Conflict-Free Replicated Data Type and fair termination of a concurrent program.
We classify various types of graded extensions of a finite braided tensor category $cal B$ in terms of its $2$-categorical Picard groups. In particular, we prove that braided extensions of $cal B$ by a finite group $A$ correspond to braided monoidal
$2$-functors from $A$ to the braided $2$-categorical Picard group of $cal B$ (consisting of invertible central $cal B$-module categories). Such functors can be expressed in terms of the Eilnberg-Mac~Lane cohomology. We describe in detail braided $2$-categorical Picard groups of symmetric fusion categories and of pointed braided fusion categories.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
