程序设计语言海外名家微型课程学习笔记

Posted on Edited on In
课程 主讲人
Introduction to Functional Programming Jeremy Gibbons
Introduction to Property Based Testing John Hughes

大纲：程序设计语言海外名家微型课程-北京大学程序设计语言研究室 (pku.edu.cn)

材料：jegi/Beijing-exercises: Exercises and other materials for the course on FP and QuickCheck at Peking University in October 2023 (github.com)

授课地点：北京大学

第一讲

Functions, equations, recursion reasoning, higher-order.

传统的有语句statement和表达式expression，函数时可以理解为只涉及表达式，只操作value，这种视角可能回更加精简。

no side effects是expression的一个重要性质

  • 赋值操作(action)会破坏这样的性质

Fortran将statement转化为一系列简单的机器操作，这在当时是一种创新，队expression的拓展

applicative order evaluation：先计算参数，再展开函数并带入【对于infinity之类的递归定义值不太好处理】

normal order evaluation：先展开函数定义，再考虑带入参数【call by need， lazy evaluation，Haskell用这个】

Haskell的函数类型定义类似$f::A\rightarrow B$，$f$是函数名，$A$和$B$是参数类型，调用函数的时候$f\ x$即可，例如
$$
square::Integer\rightarrow Integer\
square\ (3+4)
$$
用lambda表达式写square就是$\lambda x\rightarrow x\times x$

Haskell支持多种编程风格，declaration style和expression style

函数相等的含义是说对于任何输入的参数，函数都能输出相同的内容【当然计算机不能知道】

Currying：把结构化的参数替换为多个更简单的结构，函数的柯里化。例如把一个接受两个参数的函数转化为一个接受两个连续参数的函数。

所谓的接受两个连续参数，定义可以写成$f::Integer\rightarrow Integer\rightarrow Integer$，它等价于$f::Integer\rightarrow (Integer\rightarrow Integer)$【右结合性】，也就是先接受一个参数，返回一个函数，再由这个函数接受连续的第二个参数。实际调用的时候可以写成$fa\ b$

associative：可以随便加括号，例如+*等。而FP中函数类型定义的操作符$\rightarrow$是右结合的，函数调用则是左结合的，所以特别的顺序需要额外加括号

composition：函数复合，$f\circ g=\lambda x\rightarrow f(g\ x)$，即先调用$g$再调用$f$,显然它是associative的

definitions：例如
$$
here::String\
here=\text”Oxford\text”\
smaller::(Integer, Integer)\rightarrow Integer\
smaller\ (x,y)=\bold{if}\ x\le y\ \bold{then}\ x\ \bold{else}\ y
$$
“=”意味着pattern match，即等号左边的pattern可以替换为右边的内容。所以你可以定义特殊情况的替换规则。等号右侧的表达式中可以引入新变量，并在最后用where语句写local definition
$$
foo::Float\rightarrow Float\
foo\ x = x + a\ \bold{where}\ a=sqrt\ x
$$
也可以使用$\bold{let}\ definition\ \bold{in}\ expression$的形式

一些有趣的定义：
$$
curry::((a,b)\rightarrow c)\rightarrow(a\rightarrow b\rightarrow c)\
curry\ f=\lambda a\ b\rightarrow f(a,b)
$$
根据定义，curry接受一个$((a,b)\rightarrow c)$函数，返回一个$(a\rightarrow b\rightarrow c)$的函数。对应到下面，$f$就是这个参数，而等号右边的$\lambda\cdots$就是返回的函数。这个返回的函数接受两个参数，返回参数$f$调用这两个函数的结果。
$$
iter::Int\rightarrow (Integer\rightarrow Integer)\rightarrow(Integer\rightarrow Integer)\
iter\ 0\ f=id\
iter\ n\ f=f\circ iter(n-1)\ f
$$

Motivational introduction to property-based testing, with stories from the battlefield—using Quviq QuickCheck for Erlang

generate tests but write them

Example：a Circular Buffer，一个用C实现的循环buffer，通过取模运算实现

property：size大小应该正确

计算size的时候需要%size，但是如果实占空间(input pointer - output pointer)==size，那么结果是0=>不正确。

  • 解决方法：偷偷将size在分配时搞成n+1，这样实占n的时候n%(n+1)也能得到正确结果

如果input pointer在output pointer之前，%会产生负数结果。

  • 解决方法：(input pointer - output pointer + size) % size

有状态机器模型

每个API call有pre condition/stste transition/post condition，call完以后的post condition应该与对应model一致

  • 同一个property可以测出不同的bug
  • 精简失败的测试样例可以使我们debug变得更简单

CANbug的例子：底层由于ID的bit长度不够用而拓展长度，让最左边的bit作为标志版本位，结果软件工程师在比较priority时却从左边开始比。

state model machine该如何应对并发情况呢？可能结果太多了

他的解释是以可能的sequence作为model，因为大多数的操作是原子的，可以这样干

Q: dif between fuzzing and pbt?

A: 也有一些用coverage based 方法来做pbt的

第二讲

Algebraic datatypes

list：

import Data.List

$[1,2,3],[]$，用$ele:list$表示ele后面接续的list。$[1,2,3]=1:2:3:[]$

同一函数的多个pattern matching可以用case of语句结合起来

list操作符：$++::[Integer]\rightarrow[Integer]\rightarrow[Integer]$两个拼接，$concat::[[Integer]]\rightarrow[Integer]$，$reverse$

map：对每个ele执行操作
$$
map::(Intger\rightarrow Integer)\rightarrow [Integer]\rightarrow[Integer]\
map\ f(x:xs)=f\ x:map\ f\ xs
$$
filter：
$$
\begin{align}
filter\ p(x:xs)\
&|p\ x&=x:filter\ p\ xs\
&|otherwise&=filter\ p\ xs
\end{align}
$$
list-generating expression: $[e|Qs]$，e是表达式，Qs是用”,”分割一系列qualifier，例如$x\leftarrow xs$这样的generator，或者其他条件

x:xs这样的格式让haskell的列表更加适用于类似于动规那样可以分解为子问题的算法

Fold right：类似sum x:xs=x+sum xs这种，展开后从右向左合并

Fold left：foldl op e (x:xs) = foldl op (e ‘op’ x) xs展开后(((e op x)op y) op x ……从左向右合并。即先提供一个初始值e，然后不停用op操作已有值与第一个值

【？？漏了】

algebraic datatypes：用代数形式表示的数据类型，例如一个接受A类型和B类型的函数C接受参数后可以视为一份Data，再例如一些类型的复合等等

How to specify it!

propert check函数可以使用===才判断相等的同时展示相关信息

import Test.QuickCheck

prop_Reverse :: [Integer] -> [Integer] -> [Integer] --明确的类型告诉QuickCheck怎么生成test
prop_Reverse xs ys = reverse (xs ++ ys) === reverse ys ++ reverse xs

ghci中quckCheck prop_Reverse

但是如果我们本身就不知道返回值的正确结果，如何写测试代码呢？

  • 可以用返回值的property继续处理 ppt p6
  • 但是可能不够精确，导致测不出bug！ppt p7

5 systematic ways of formulating properties

荐书：《How to Solve It》

RQs：

  • invariant，不变的性质等等。可以将不变性套用到要测的相关操作上
  • postcondition，发生操作之后，condition可以用操作的参数以及原数据等表示。通过construct这些操作来确保相关性质一定成立(不涉及可能有问题的逻辑)
  • metamorphic tests，对测试进行变质，不同测试顺序达到相同结果or性质
  • inductive properties，可以归纳证明其他相关操作正确性的基础性质
  • model based properties，对程序状态建模model(自动生成)，需要确保模型正确，程序状态变迁的同时model自己变迁，比对新程序状态是否能转为新model

第三讲

Types, polymorphism, type classes

Algebraic Data Type(ADT)：复合数据类型，例如$\bold{data}\ Person=P\ Name\ Age$。这里$P$就可以看作一个constructor(类似$Just$等)，Person作为参数的时候，可以用$(P\ …\ …)$代替。

ADT也可以是递归的，例如$\bold{data}\ Expr=Lit\ Integer|Add\ Expr\ Expr$

Nat和List的定义也是递归数据结构，可以参考ppt

Haskell是强类型语言，类型的检查在执行之前。所以即便False && 1(短路)也是会报错的

多态：例如$fst::(x,y) \rightarrow x$中的x,y可以指代任何类型

如果函数$h::[a]\rightarrow[a]$不涉及其他元素，只会rearrange原本列表中的元素。这就带来了一个有趣的性质：$map\ f\circ h=h\circ map\ f$【free theorem】

type classes：为泛型加上约束，类型一定要在这一组类里，例如$(+)::(Num\ a)=>(a\rightarrow a\rightarrow a)$

Generators

QuickCheck的class Arbitrary a有两个属性(这里a是泛型)

  • arbitrary：类型为Gen a，产生一个随机的a

  • shrink：根据生成的数据，产生shrinking的备选List::[a]。shringing时不停选用其中最靠前且能导致当前case仍然fail的元素替换x，如果没有，则将case设为shrunk case

Type modifier：使用type约束参数以增加generate的效率，为了方便类型检查和可读性，可以使用new type

四个可用的Gen的Combinator：

  • $choose\ (m,n)$
  • $element\ xs$
  • $onof\ [gen1,\cdots, genN]$
  • $frequency\ [(w1, gen1),\cdots,genN]$

test Arbitary/Shrink？generator和shrink可能使用了buggy code，所以要先保证generator的正确

sized generator，给generator加额外的参数，更加自定义化

如果树和k分别用Int生成的话，效率可能会很低，

generate Key in the same way P40

我们建立一个新的类型Key，从而Key的 Arbitrary生成遵循同一种方式，并且利用一些方法将范围尽可能的缩小，从而使效率尽可能地高

更加精细化的label设置，使样例的统计更加合理

如果对测试的占比有要求，可以使用cover算子 cover expected_percentage condition label

第四讲

Monads and Applicative Functors

side effect？？和主计算逻辑关联不大的的一些事

Monad：模拟顺序执行的一种函数式hack，可以帮助实现IO等有副作用的执行

传统的方式会将副作用逻辑与值逻辑混合起来，造成程序结构的混乱
$$
\bold{class}\ Monad\ m\ \bold{where}\
return::a\rightarrow m\ a\
(>>=)::m\ a\rightarrow(a\rightarrow m\ b)\rightarrow m\ b
$$
这里m可以理解为某种computation

bind：do this，用结果do that，然后得到一个结果

由于bind中有各步执行的结果，所以可以模拟顺序执行语言。

$\bold{do}$语法糖可以帮助自动生成bind等，在其中使用$\leftarrow$来表达类似赋值的语义(实际是赋予monad 内部的值)。

IO Monad：输入输出/文件……

Applicative functors是弱一点的定义，Monad是Approach【licative的

Traversal

State machine models in Haskell

程序的输入来自一个外部的复杂系统(OS/DB……)，输出也输出到这个复杂系统。我们无法随时建模复杂系统，但是可以有初始状态

model/action

needs：为了记录哪些step需要记录下来

然后perform以[Ret stat]作为一个参数来解决之前的问题

在test开始时清理系统保证test不会受之前的test影响

negative test：需要测试出故意设置的错误的样例

第五讲

Laziness and Infinite Data Structures

lazy evaluatiion：共享计算结果，而不是单纯的复制。即haskell先将函数展开，但是对于需要被计算出的值延迟到计算到这里的时候再算。从而可以在实现无限的数据结构的基础上，计算出优先结果(在有限步内)

QuickSpec——Formal Specifications for Free

QuickSpec如何检测程序性质？枚举所有可能的等式，然后测试是否成立

对于可能有bug的程序，Quick Spec可以给出一种insight来揭示程序的性质。并且我们可以通过检查这些性质来查看程序设计是否符合我们的预期。