当前位置:网站首页>[TAPL] 概念笔记

[TAPL] 概念笔记

2022-08-10 18:23:00 SakamataZ

文章目录

基础概念

  • 什么是gradual typing
    允许一部分使用动态类型一部分使用静态类型的语言
  • type classes
    对类型进行操作的类
  • type-class polymorphic
    类型类多态,相当于type classes的接口函数
  • trait 构造顺序
    调用超类的构造器;
    特征构造器在超类构造器之后、类构造器之前执行;
    特征由左到右被构造;
    每个特征当中,父特征先被构造;
    如果多个特征共有一个父特征,父特征不会被重复构造
    所有特征被构造完毕,子类被构造。
  • trait和type classes有什么区别?
  1. typeclasses以单独的方式处理而非将对象固定到表面
  2. trait不支持functor和applicative等高阶函数
  • 什么是皮亚诺系统?什么是后继运算?什么是归纳集?什么是λ演算?β系统中α和β两种变换分别是什么?
    https://zhuanlan.zhihu.com/p/34679052
    要注意的是:给λ演算的语法项符号不同的推导规则,得到的公理系统也不同,其中最简单的是β系统,它指定了α和β两种变换
  • 什么是卫生宏?
    lisp引入的宏规则,
  1. 宏展开后,原表达式处于新的词法环境中
  2. 宏展开式中的自由标识符,处于宏定义时的词法作用域中,保留其引用透明性
  • 为什么Rust比C++慢?
    1.没有RVO 返回类型优化防止新的临时对象创建 2.Arc不能去掉弱引用计数 3.如果不优化move,那么会多占用栈空间 4.没有placement new,不能在已分配的内存中分配对象。

TAPL

  • 评估形式化语义的三种方法是什么?
    评估形式化的语义,就是评估项term的语义,
    主要有:
    操作语义(将语言视为抽象的自动机)
    指称语义(定义一集数学的对象domains,并且定义一个解释函数,将terms映射到domains实体中)
    公理化语义(公理化语义从定义的自身出发推导出语言的含义)

  • one-step evaluation relation:
    满足规则的最小二进制关系

  • 什么是mutable reference cells 和 nonlocal exception handling?

  • 类型系统是指一种根据计算出的值的种类对于词语进行分类,从而证明某程序行为不会发生的可行语法手段。

  • 给定语言中能够使用类型系统消除的错误一般称为运行时类型错误runtime type error,一般的类型系统相对直接的检查能够校验简单的类型错误和数组越界。

  • 一个类型安全的语言是编程时不会危害到自身的语言,是一个保护其抽象的语言,

  • 语言安全性可以由运行时或静态类型检查保证,Scheme没有静态检查,但是仍然类型安全。如果建立了动态检查的设施,那么检查的代价将会很小(但是也存在一些Basic方言 提供底层原语,因此不安全)

  • 不安全的语言通常提供效果最佳的静态类型检查器,但是一般不能够保证良类型的程序是良行为的

  • 在对象变量上取值的变量称为元变量,不含自由变量的项称为封闭项,封闭项也称为组合子,最简单的组合子称为恒等函数 id = lambdax(x)只输出其变元。 不动点组合式可以用来定义递归函数

  • full beta规约:任何时候可以以任意顺序规约 规范顺序

  • normal order策略:最左侧最外面先被规约

  • 按名调用call by name:不针对抽象进行规约。

  • haskell采用按需规约call by need的方式
    一般则采用call by value的方式

  • 使用lambda项表示的数称之为church数值 Church 编码是一种“抽象方法”,它将“数字”、“运算”等概念全数“抽象”成λ- 演算

  • 简单代换一个项x到t,使自由变量编程收到限制的变量的情况称为变量捕捉

  • 纯lambda演算是图灵完备的,为了解决结果的发散问题,有两种方案,第一种使用项的类型注释来显式检查类型的结果,第二种是使用类型检查器自己推导或者重构这个信息。

原网站

版权声明
本文为[SakamataZ]所创,转载请带上原文链接,感谢
https://blog.csdn.net/treblez/article/details/126210869