1

我面前的盘子里装了3个苹果，我说：这盘子里有三个苹果。你看了一眼说，对。

这里不需要证明，“所见即所得”，看就能确认

假如对方是盲人，我说“你前面桌上的盘子里放着3个苹果”。他就要摸摸，摸到了才能确认

或者摸到盘子，摸到一个苹果，就拿出来，然后再摸再拿，直到摸到盘子空了，计数为3.则可确认盘子里有3个苹果

计算机就是这瞎子（别说计算机视觉），切不可直接把人的感觉带入计算机，那就是人性的，太人性的了

2

从一个标有“桔子”的袋子里不确定能取出什么，也许会是一把手枪

如果有个前提：东西会放到标有其名称的相应的袋子中，那就能确定从标有“桔子”的袋子里取出的就是桔子

一个显式的（静态）类型系统，既然首先构造了类型，按类型构造了值，所以能确认该值属于某个类型

3

类型的构造方式

(1)明确构造的类型

（2）字面量标识的类型。（是什么样子就是什么）

剩下的，只有相应的处理该类型的函数都通过了，才能说明该值是此类型

{:a 1 :b 2 :c 3}

我能说“这是”一个clojure map吗？其实我只能说我看到了一个map,我相信我写了一个map

1 我看到了一个map,但我的确是可能看错的，我认为我写了一个{:a 1 :b 2 :c 3}，但的确有可能我写的是{:a 1 :b 2 c 3}我忘了写c前面的冒号了

2 我相信我写对了，当然，人都首先是相信自己是对的

要说明这的确是个map,只有处理map的函数都能正确运行才行