Scheme/Lisp有類型系統嗎？

02-06

看王垠一直在批評Haskell的Hindley-Milner等等，想問問Scheme/Lisp這樣的語言如何

當然有啊，滿屏的 $exists$

王垠如何先不談，動態類型系統實際上也是靜態類型系統的一種。如果一個語言里所有的值都只有一種類型，那麼這種語言的類型系統就被稱為動態類型系統。

比如以簡化的Scheme為例，

data Value = Fixnum Int | Symbol String | Cons Value Value | Nil | T | F

無論是數字，符號，列表，都是一種類型。

在此之上寫一個big-step的解釋函數

eval :: Value -&> Value

就留作作業了：）

擴展閱讀：

Dynamics Language Are Static Languages

Benjamin Pierce: Types and Programming Languages

Write Yourself a Scheme in 48 Hours

王垠和他的老師 Friedman 一樣「不喜歡一切複雜的東西。」

scheme的作者Sussman說 scheme 是也有類型系統的，但是程序員要自己記住對象的屬於類型。。。。。

==========

略有有篡改逃）

scheme方言racket有typed-racket.可以在racket中使用類型系統

* lisp的類型

從lisp七條公理的角度出發

quote
atom?
eq?
car
cdr
cons
cond

可以發現，lisp其實只有這樣幾個類型：

空，即 (quote ())，有很多方言把它叫做 nil什麼的
atom, 即(quote symble) 這樣的，可以用atom?來判斷
然後還有一個類型就是bool類型，即eq? atom?這種操作的結果
pair, 即用cons構造的那個數據結構。

* lisp做強類型檢查么？

我覺得這要看怎麼實現的：

比如，

A. (quote ()) 是不是 atom
B. cond的時候，(quote ()) 是不是當做假
C. cond裡面，非(quote ())的atom是不是當做真
D. cond裡面，所有的pair是不是都當作真

而且進一步說，就算以上的回答是 yes, 也可能是做了類型推斷的結果。

* 那整數、字元串、浮點數這些是怎麼回事？

比如我可以這樣來構造自然數：

;; #f是bool類型，表示false, #t是bool類型，表示true, add是 (quote add)的縮寫。 ;; reverse我就不定義了 (define #f (eq? a b)) (define #t (eq? a a)) (define (and x y) (cond (x (cond (y #t) (#t #f))) (#t #f))) (define (not x) (cond (x #f) (#t #t))) (define (null? x) (eq? x ())) (define (reverse x) (let lp ((r ()) (y x)) (cond ((null? y) r) (#t (lp (cons (car y) res) (cdr y))))))


(define (nature-number x)

   (let ((n x))

      (lambda (op . y)

         (cond ((eq? op add)

       (let lp ((res ()) (f #f) (rx x) (ry y))

   (let ((cx (cond ((null? rx) #f) (#t (car rx))))

                          (cy (cond ((null? ry) #f) (#t (car ry))))

                          (rex (cond ((null? rx) ()) (#t (cdr rx))))

                          (rey (cond ((null? ry) ()) (#t (cdr ry)))))

(cond ((and (null? rex) (and (null? rey) (not f))) res)

                               (#t

       	       (cond ((and cx (and cy f)) (lp (cons #t res) #t rex rey))

                                    ((and (not cx) (and cy f)) (lp (cons #f res) #t rex rey))

                                    ((and cx (and (not cy) f)) (lp (cons #f res) #t rex rey))

                                    ((and cx (and cy (not f))) (lp (cons #f res) #t rex rey))

                                    ((and (not cx) (and (not cy) f)) (lp (cons #t res) #f rex rey))

     	                            ((and (not cx) (and cy (not f))) (lp (cons #t res) #f rex rey))

     	                            ((and cx (and (not cy) (not f))) (lp (cons #t res) #f rex rey))

                                    ((and (not cx) (and (not cy) (not f))) (lp (cons #f res) #f rex rey))))))))))))
(define (+ x y) (reverse (x add y)))

; 以上定義的是自然數加法，自然數的表達是 (#t #f #t #t) 的二進位，而且是big endian。

從上面的定義看到，這個加法其實沒有對y做任何類型檢查。

如果y是這樣一個 list : (a (b c) () d)的話，

如果

A. cond認為 a b (b c)都是 #t, 而()是#f的話，那麼y就變成 ( #t #t #f #t)了

B. cond做強類型檢查，報錯的話，那麼上面的加法就做不成了

以上的 A 就是一種類型推斷， B就是強類型檢查。

同理可以定義減法，然後就有了整數，然後定義乘法和除法，就可以定義有理數，再然後就可以定義實數了，以及整個數學系統。這個大約就是類型論的出發點吧。

直接點回題主的問題：王垠不是說類型本身有問題，他說的是HM類型推斷有問題。

Typed racket應該算

基本上所有語言都有類型系統…要不你來跟我說一下字元串加整數等於幾?（JS這種自帶這種類型變換的不算）

只不過編程語言分為動態類型（運行時進行類型檢查）和靜態類型（編譯時進行類型檢查）這兩種（其實還有比較另類的，先不說），scheme是動態類型的，所以會感覺不到類型系統而已

Typed/racket

沒有可以讓它有。有可以讓它沒有。