6260 notes: tuple, type, predicate, implicate

3 minute read Published: 2026-07-29

元组 (tuple)

var 的作用类似别的语言里的 let。就是起别名的意思。（变量声明）

用:=符号，结尾要加;分号

元组把 n 个值捆成一个值，用 .0、.1 取出来（里面装什么类型都行）: 设 t = (3, 7)， t.0 就是 3， t.1 就是 7。


var t := (3, 7);

// t.0 == 3

// t.1 == 7

两种swap


function swap_ish(x: int, y: int): (int, int) {

  (y, x)

}

①x: int, y: int —— 收两个散装的整数,一个叫 x,一个叫 y

②(int, int) —— 吐出一个元组(一个装两个整数的盒子)

③函数体 (y, x) —— 造这个盒子:左格放 y,右格放 x


function swap(xy: (int, int)): (int, int) {

  (xy.1, xy.0)

}

①xy: (int, int) —— 只收一个参数,这个参数本身就是个盒子,名字叫 xy

②函数体 (xy.1, xy.0) —— 从盒子里取出右格 xy.1、左格 xy.0,反着装进一个新盒子

两者的区别:前者收两个散装的值,后者收一个已经打包好的盒子。

type: 类型的绰号

练习:两个三维向量的点积

我的最初写法 —— 给本是同一个的类型造了两个绰号:


type vector3D_1 = (int, int, int)

type vector3D_2 = (int, int, int)

  

function dot(v: vector3D_1, u: vector3D_2): int {

  v.0 * u.0 + v.1 * u.1 + v.2 * u.2

}

重点：类型是一类东西的名字,不是某个东西的名字。

正确写法只需要一个类型:


type vector3D = (int, int, int)

  

function dot(v: vector3D, u: vector3D): int {

  v.0 * u.0 + v.1 * u.1 + v.2 * u.2

}

恰如 (x: int, y: int) 不需要写成 (x: int_1, y: int_2)。况且 vector3D_1 和 vector3D_2 在机器眼里没区别。

参数:

①各有各的: 名字 ─→ 值

②可以共享: 类型 ─→ 类

谓词 (predicate)

function isEven(x: int): bool { x % 2 == 0 }

①x % 2 —— x 除以 2 的余数，为 1 或 0。6 % 2 == 0,7 % 2 == 1

②x % 2 == 0 —— 问句：余数等于 0 吗?答案为 true 或 false。

③函数体就是个问句，所以 isEven(6) 返回 true,isEven(7) 返回 false。

两个符号:

①== 是“相等吗?” —— 一个问句,产生 true 或 false

②:= 是赋值

完全等价:

function  isOdd(x: int): bool { x % 2 == 1 }
predicate isOdd(x: int)       { x % 2 == 1 }

predicate 即谓词，“关于一个对象的判断” —— isEven 和 isOdd 都是对 x 的一个判断。

predicate = 返回 bool 的 function

蕴含 `==>` (implicate)

predicate mystery(x: int) { !isEven(x) ==> true }

蕴含 ==>：只有"左真右假"才是 false,其余一律 true。左假直接判真。

x = 6:isEven(6) = true → !true = false → false ==> true → true

x = 7:isEven(7) = false → !false = true → true ==> true → true