Linear logic gives us additive pairs in the form of the additive conjunction. Intuitionistic type theory gives us dependent pairs in the form of the dependent sum type. What happens when we combine these two kinds of pairs together? And is this new pair type useful in practice? To answer these questions, we employ quantitative type theory, which can describe both substructural and dependent types simultaneously. In our previous work, we introduced dependent additive pairs. In this work, we show how these pairs can be used in three completely different scenarios: folding data structures using linear recursion schemes, computing resource-aware proofs, and defining additive versions of inductive and coinductive types. Each of these scenarios is then illustrated by an implementation in the Janus language.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Programming with Dependent Additive Pairs

  • Vít Šefl

摘要

Linear logic gives us additive pairs in the form of the additive conjunction. Intuitionistic type theory gives us dependent pairs in the form of the dependent sum type. What happens when we combine these two kinds of pairs together? And is this new pair type useful in practice? To answer these questions, we employ quantitative type theory, which can describe both substructural and dependent types simultaneously. In our previous work, we introduced dependent additive pairs. In this work, we show how these pairs can be used in three completely different scenarios: folding data structures using linear recursion schemes, computing resource-aware proofs, and defining additive versions of inductive and coinductive types. Each of these scenarios is then illustrated by an implementation in the Janus language.