【PL理论】(34) 类型系统:不完备性 | 为什么推导树推导失败? | 实现类型系统 | 调整到类型系统 | 思考:强制程序员写类型还是自动推断类型?

  •  💬 写在前面:回顾我们的目标是为 F- 语言设计一个完备但不完全的类型系统,本章我们探讨的主题是类型系统的完备性。

目录

0x00 类型系统的不完备性

0x01 为什么推导树推导失败?

0x02 实现类型系统

0x03 调整到类型系统

0x04 思考:强制程序员写类型还是自动推断类型?


0x00 类型系统的不完备性

完备性属性可以描述如下:如果 𝝓 ⊢ 𝒆 ∶ 𝒕 成立,则程序 𝒆 不会出现类型错误。

同时,如果该程序终止并输出 𝒗 作为结果,则 𝒗 的类型是 𝒕

(注意,𝝓 ⊢ 𝒆 ∶ 𝒕 并不保证程序一定会终止)

下面我们来讨论一下类型系统的 不完备性 (Incompleteness)。

可能存在一些程序,即使没有任何类型错误,我们的类型系统也无法接受。

存在这样的程序 𝒆,使得对于某个𝒗,𝝓 ⊢ 𝒆 ⇓ 𝒗 成立,但对于任何𝒕,𝝓 ⊢ 𝒆 ∶ 𝒕 都不成立。比如 if true then 1 else false,再比如 let f x = x in if (f true) then (f 1) else 2

我们当前的类型系统不支持这种多态性:稍后我们将简要讨论这个问题。

0x01 为什么推导树推导失败?

\color{}f 不能同时是 \color{} int \rightarrow int\color{}bool \rightarrow bool

即使将 \color{}f 保持为 \color{}{}'a \rightarrow {}'a 类型也不能解决这个问题。

0x02 实现类型系统

到目前为止我们讨论过的类型规则 (𝚪 ⊢ 𝒆 ∶ 𝒕) 是我们类型系统的规范。

对于给定的程序 𝒆,如果存在某个类型 𝒕 使得 𝝓 ⊢ 𝒆 ∶ 𝒕 成立,那么我们的类型系统必须接受 𝒆。

如果不存在这样的类型 𝒕,则我们的类型系统将不接受 𝒆。

现在,让我们考虑如何实际实现它,我们应该如何编写这个类型系统的代码?

回顾一下解释器,当我们编写 F- 解释器时,语义可以很容易地通过递归实现。

我们可以直接将 𝝆 ⊢ 𝒆 ⇓ 𝒗 的定义翻译成代码 (就像下面的例子那样)

对于类型系统,我们是否也可以这么做呢?

let rec evalExp(exp: Exp) (env: Env) : Val =match exp with| LetIn(x, e1, e2) ->let v1 = evalExp e1 envevalExp e2(Map.add x v1 env)| ...

0x03 调整到类型系统

你可能会认为我们可以做同样的事情,对大多数情况而言,这是有效的。

如下例所示,注意下面的代码 (看起来是不是很类似于解释器的代码?):

let rec typeOf (exp: Exp) (tenv: TyEnv) : Typ =match exp with| LetIn (x, e1, e2) ->let t1 = typeOf e1 tenvtypeOf e2 (Map.add x t1 tenv)| ...

0x04 思考:强制程序员写类型还是自动推断类型?

下面的类型规则中,我们无法通过递归来确定参数类型 \color{}t_a

在绘制推导树时,你可以用 "直觉" 来理解,但计算机是如何做到的?

let rec typeOf (exp: Exp) (tenv: TyEnv) : Typ =match exp with| LetFunIn (f, x, e1, e2) ->let ta = ??? // 这里我们应该做啥?let tr = typeOf e1 (Map.add x ta tenv)typeOf e2 (Map.add f (ta → tr) tenv)| ...

一个可能的解决方案是 —— 强制程序员写出参数类型(let f (x: int) = ...)

"程序员何必为难程序员……"

不然的话,我们就需要一个算法来 自动推断类型 了,我们会在下一章进行讲解!

📌 [ 笔者 ]   王亦优
📃 [ 更新 ]   2024.6.14
❌ [ 勘误 ]   /* 暂无 */
📜 [ 声明 ]   由于作者水平有限,本文有错误和不准确之处在所难免,本人也很想知道这些错误,恳望读者批评指正!

📜 参考资料 

- R. Neapolitan, Foundations of Algorithms (5th ed.), Jones & Bartlett, 2015.

- T. Cormen《算法导论》(第三版),麻省理工学院出版社,2009年。

- T. Roughgarden, Algorithms Illuminated, Part 1~3, Soundlikeyourself Publishing, 2018.

- J. Kleinberg&E. Tardos, Algorithm Design, Addison Wesley, 2005.

- R. Sedgewick&K. Wayne,《算法》(第四版),Addison-Wesley,2011

- S. Dasgupta,《算法》,McGraw-Hill教育出版社,2006。

- S. Baase&A. Van Gelder, Computer Algorithms: 设计与分析简介》,Addison Wesley,2000。

- E. Horowitz,《C语言中的数据结构基础》,计算机科学出版社,1993

- S. Skiena, The Algorithm Design Manual (2nd ed.), Springer, 2008.

- A. Aho, J. Hopcroft, and J. Ullman, Design and Analysis of Algorithms, Addison-Wesley, 1974.

- M. Weiss, Data Structure and Algorithm Analysis in C (2nd ed.), Pearson, 1997.

- A. Levitin, Introduction to the Design and Analysis of Algorithms, Addison Wesley, 2003. - A. Aho, J. Hopcroft, and J. Ullman, Data Structures and Algorithms, Addison-Wesley, 1983.

- E. Horowitz, S. Sahni and S. Rajasekaran, Computer Algorithms/C++, Computer Science Press, 1997.

- R. Sedgewick, Algorithms in C: 第1-4部分(第三版),Addison-Wesley,1998

- R. Sedgewick,《C语言中的算法》。第5部分(第3版),Addison-Wesley,2002

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/news/856560.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

动态轮换代理在多账户管理中有何用处?

如果您要处理多个在线帐户,选择正确的代理类型对于实现流畅的性能至关重要。但最适合这项工作的代理类型是什么? 为了更好地管理不同平台上的多个账户并优化成本,动态住宅代理IP通常作用在此。 一、什么是轮换代理? 轮换代理充当…

德语中常见的日常用语,柯桥哪里可以学德语

Das kommt mir spanisch vor. (直译:这对我来说很西班牙。) Das kommt mir spanisch vor. Man findet etwas seltsam und ist unsicher, was man glauben soll. 这对我来说很西班牙。 某物让人觉得很稀奇,人们不确定自己该相…

泰山众筹:电商创新模式引领双赢时代

一、泰山众筹:电商领域的新星 泰山众筹,作为电商领域的一股创新力量,凭借其独特的商业模式在市场中崭露头角。这一模式巧妙地将产品销售与积分众筹融为一体,为用户和平台创造了互利共赢的机遇。在泰山众筹的平台上,用…

北方高温来袭!动力煤却不涨反跌的原因分析

内容提要 北方高温而南方降雨偏多的格局或将继续,整体水力发电量增长可能继续明显增长,但火电增幅可能继续缩小。5月重点火电厂的发电量和耗煤量增速均呈现负增长,耗煤量月度同比下降7%,而重点水电同比大增近40%。我国电力行业绿…

2020年中国1km格网耕地破碎度数据集

摘要 耕地破碎度是对耕地破碎化的定量描述,耕地破碎化是指由于自然或人为因素,耕地图斑数量增加,斑块大小减小,隔离程度增加,呈现出分散和无序格局。破碎化不仅会影响生态系统的结构和功能,同时不利于提高耕…

深度学习模型训练中 学习率参数 设置大小问题及设置合适值

💪 专业从事且热爱图像处理,图像处理专栏更新如下👇: 📝《图像去噪》 📝《超分辨率重建》 📝《语义分割》 📝《风格迁移》 📝《目标检测》 📝《暗光增强》 &a…

聊聊探索性测试

探索性测试定义及来源:​ 特意度娘了一下,探索性测试的定义: 探索性测试可以说是一种测试思维技术。它没有很多实际的测试方法、技术和工具,但是却是所有测试人员都应该掌握的一种测试思维方式。探索性强调测试人员的主观能动性…

解决跨域问题,过滤器Filter,Servlet容器最重要的技术之一(基于SpringBoot开发过滤器)

注:本文中Tomcat,代表所有的Serlvet容器,由于Tomcat非常流行,所以用这个读者更加熟悉。 一、过滤器是什么,有什么用 你完成了项目编写,把它发布到网络上运行,此时,外部主机可以访问…

go sync包(二) 互斥锁(二)

互斥锁 Mutex mutex 的 加解锁很简单: var mutex sync.Mutexmutex.Lock()defer mutex.Unlock()// 加锁期间的代码逻辑加锁 // Lock locks m. // If the lock is already in use, the calling goroutine // blocks until the mutex is available. func (m *Mutex) …

机房布线新方案:数字化运维如何助力企业高效腾飞

随着信息量的激增,传统的机房布线管理方式已经难以满足现代化企业的需求,存在着“视觉混乱、记录不准”等严重问题,这不仅影响了机房运维的效率,更对企业的数据安全构成了潜在威胁。然而,随着耐威迪数字化运维管理方案…

工业AIoT竞赛

模块一:工业物联环境构建 # 查看节点状态 kubectl get nodes # 查看所有 pods 状态 kubectl get pods --all-namespaces cd /data/script/ ls | grep install_openyurt_manager # ./install_openyurt_manager_v5.sh是搜索到的脚本文件 ./install_openyurt_manager_v…

校园疫情防控健康打卡系统

摘 要 自疫情出现以来,全世界人民的生命安全和健康都面临着严重威胁。高校是我国培养人才的重要基地,其安全和稳定影响着社会的发展和进步。因此,各高校高度重视疫情防控工作,并在校园疫情防控中引入了健康打卡系统。本论文主要研…

tsf consul单独使用,可以在tsf部署不

Consul 是一个开源的工具,用于服务发现和配置。它提供了服务注册与发现、健康检查、键值存储、多数据中心支持等功能。Consul 可以单独使用,也可以与其他系统集成,如与微服务平台 TSF(Tencent Service Framework)结合使…

RISC_CPU模块的调试

代码: cpu.v include "clk_gen.v" include "accum.v" include "adr.v" include "alu.v" include "machine.v" include "counter.v" include "machinectl.v" include "register.v&quo…

小兔鲜02

elementplus自动按需引入 elementplus主题色定制 安装sass npm install sass -D要替换的主题色内容: /* 只需要重写你需要的即可 */ forward element-plus/theme-chalk/src/common/var.scss with ($colors: (primary: (// 主色base: #27ba9b,),success: (// 成功…

【前端项目笔记】4 权限管理

权限管理 效果展示: (1)权限列表 (2)角色列表 其中的分配权限功能 权限列表功能开发 新功能模块,需要创建新分支 git branch 查看所有分支(*表示当前分支) git checkout -b ri…

Python字典常用操作与进阶玩法

在Python中,字典是一种常用的数据结构,是实现各类算法的基础。 1.创建字典 有多种方法可以创建字典,以下几种方法创建的字典均等于 {"one": 1, "two": 2, "three": 3} a dict(one1, two2, three3) b {one:…

审稿人:拜托,请把模型时间序列去趋势!!

大侠幸会,在下全网同名「算法金」 0 基础转 AI 上岸,多个算法赛 Top 「日更万日,让更多人享受智能乐趣」 时间序列分析是数据科学中一个重要的领域。通过对时间序列数据的分析,我们可以从数据中发现规律、预测未来趋势以及做出决策…

web中间件漏洞-Resin漏洞-密码爆破、上传war

web中间件漏洞-Resin漏洞-密码爆破、上传webshell 使用爆破结果resin/resin进入后台,选择deploy。想部署webshell,得使用SSL方式请求,访问https://192.168.1.2:8443/resin-admin/index.php?qdeploy&s0(注:如果使用最新的火狐浏览器或者谷…

vb.net帮助文档

vb.net帮助文档:https://download.csdn.net/download/wgxds/89462555