This paper considers parametricity and its consequent free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the level of terms, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate and challenging. In particular, to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We also prove that our model satisfies an appropriate Abstraction Theorem, as well as that it verifies all standard consequences of parametricity in the presence of primitive nested types. We give several concrete examples illustrating how our model can be used to derive useful free theorems, including a short cut fusion transformation, for programs over nested types. Finally, we consider generalizing our results to GADTs, and argue that no extension of our parametric model for nested types can give a functorial interpretation of GADTs in terms of left Kan extensions and still be parametric.


翻译:本文审视了嵌入数据类型的近似度及其随后的免费理论。 我们不是在系统F的更高类型或依附型扩展中通过教会编码代表嵌入类型。 我们采取功能性编程视角, 并设计了Hindley- Milner风格的计算器, 以原始方式直接建造嵌入类型作为固定点。 我们的计算仪可以明确显示文献中出现的所有嵌入类型, 包括真正的嵌入类型。 在术语层面, 它支持原始模式匹配、 地图功能和嵌入类型折叠组合。 我们的主要贡献是构建一个我们计算系统精度更高或依附型扩展的参数模型。 这既微妙又具有挑战性。 特别是为了确保存在能解释嵌入型类型的精度固定点, 从而为我们的缩入类型建立合适的身份扩展器。 我们的计算系统必须明确跟踪各种类型, 包括真正嵌入型类型, 以及解释这些类型时的缩略图的缩略图条件, 在整个建模中, 仍然可以适当地排列。 我们还证明我们的模型能够满足一个适当的缩缩缩缩缩模型, 将模型的缩缩图, 用来解释结果, 用来解释。

0
下载
关闭预览

相关内容

iOS 8 提供的应用间和应用跟系统的功能交互特性。
  • Today (iOS and OS X): widgets for the Today view of Notification Center
  • Share (iOS and OS X): post content to web services or share content with others
  • Actions (iOS and OS X): app extensions to view or manipulate inside another app
  • Photo Editing (iOS): edit a photo or video in Apple's Photos app with extensions from a third-party apps
  • Finder Sync (OS X): remote file storage in the Finder with support for Finder content annotation
  • Storage Provider (iOS): an interface between files inside an app and other apps on a user's device
  • Custom Keyboard (iOS): system-wide alternative keyboards

Source: iOS 8 Extensions: Apple’s Plan for a Powerful App Ecosystem
如何构建你的推荐系统?这份21页ppt教程为你讲解
专知会员服务
64+阅读 · 2021年2月12日
不可错过!华盛顿大学最新《生成式模型》课程,附PPT
专知会员服务
63+阅读 · 2020年12月11日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Python分布式计算,171页pdf,Distributed Computing with Python
专知会员服务
107+阅读 · 2020年5月3日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
CCF推荐 | 国际会议信息6条
Call4Papers
9+阅读 · 2019年8月13日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
计算机 | IUI 2020等国际会议信息4条
Call4Papers
6+阅读 · 2019年6月17日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
人工智能 | SCI期刊专刊信息3条
Call4Papers
5+阅读 · 2019年1月10日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
计算机类 | 11月截稿会议信息9条
Call4Papers
6+阅读 · 2018年10月14日
人工智能 | 国际会议截稿信息5条
Call4Papers
6+阅读 · 2017年11月22日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Arxiv
0+阅读 · 2021年3月10日
Arxiv
0+阅读 · 2021年3月9日
Adversarial Metric Attack for Person Re-identification
Arxiv
4+阅读 · 2018年1月15日
VIP会员
相关VIP内容
如何构建你的推荐系统?这份21页ppt教程为你讲解
专知会员服务
64+阅读 · 2021年2月12日
不可错过!华盛顿大学最新《生成式模型》课程,附PPT
专知会员服务
63+阅读 · 2020年12月11日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Python分布式计算,171页pdf,Distributed Computing with Python
专知会员服务
107+阅读 · 2020年5月3日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
CCF推荐 | 国际会议信息6条
Call4Papers
9+阅读 · 2019年8月13日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
计算机 | IUI 2020等国际会议信息4条
Call4Papers
6+阅读 · 2019年6月17日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
人工智能 | SCI期刊专刊信息3条
Call4Papers
5+阅读 · 2019年1月10日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
计算机类 | 11月截稿会议信息9条
Call4Papers
6+阅读 · 2018年10月14日
人工智能 | 国际会议截稿信息5条
Call4Papers
6+阅读 · 2017年11月22日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Top
微信扫码咨询专知VIP会员