使用宏給racket加類型

02-09

前言：

首先，感謝@qww6 解答了我許多問題，如果有任何問題，可以在下面的評論區提出。

一直以來，racket語言因為沒有靜態類型系統而為人詬病，不少人認為這門語言辣雞。但是，racket中遠比scheme強大的宏系統帶給我們了一線希望，我們可以通過宏給racket加類型，而且不需要等待官方更新typed racket，就可以給我們的type system加上各種各樣的功能。

目前已知的給racket加類型的方法至少有兩種：1.Typed Racket所採用的將程序展開為core form後進行類型檢查的方法。

2.Type System as Macros 中所提到的一邊展開一邊檢查的方法（type tailoring）。

我們這篇文章的採用的方法是第二種。

前置知識：

我們的讀者至少應該已經了解並會使用scheme中的syntax-case宏（不會的點這裡：Syntactic Extension）

由於我們要對類型進行檢查，所以我們必須攔截所有的app，racket中提供了一個#%app的形式，所有的函數應用都會被轉化為(#%app func . args)的形式。

類似的，我們可以用重寫lambda宏，#%datum的形式來進行類型檢查。

(provide (rename-out [app #%app]))(define-syntax (app stx) (syntax-case stx () [(_ func . args) #(#%app func . args)]))

相關鏈接：17.1 Module Languages

我們的簡易類型系統:

我們將會在下面實現一個簡單的類型系統，它將支持以下類型：

type=int|string|bool|(-> type type ...)

看起來確實很簡陋啊，但是這是一個從沒有靜態類型系統到有靜態類型系統的質變。

另外，我們的類型系統不支持自動的currying（scheme傳統）。

除此之外，我們還將支持對我們程序的一些優化。

常量的類型：

給程序中出現的數字，字元串和布爾值加上類型是極為簡單的，我們只需要插進#%datum就行了，最後，我們用syntax-property(12.7 Syntax Object Properties)給typing terms加上類型信息。

(require (for-syntax syntax/parse))(provide (rename-out [app #%app][datum #%datum])) (define-syntax (datum stx) (syntax-parse stx [(d . c:integer) (syntax-property #(#%datum . c) type #int)] [(d . c:boolean) (syntax-property #(#%datum . c) type #bool)] [(d . c:str) (syntax-property #(#%datum . c) type #string)] [(d . any) (raise-syntax-error type-system-error "Dont Support this type." #any)] ))

相關鏈接（syntax-parse）：1.3 Parsing Syntax

一些primitive operator的類型：

我們這個類型系統還支持一些primop，它們是+,-,*,/,string-append,and,or,not(注意了，這裡and和or是宏，不是函數，我們必須要對它們做額外的檢查）。

我們將會用到identifier macro的知識：16.1 Pattern-Based Macros，為了方便，我們寫一個macro-transformer實現相同的功能。

(define-for-syntax (make-val-transformer val) (lambda (stx) (syntax-case stx () [_ (identifier? stx) val] [(_ . args) #`(app #,val . args)])))

對於簡單的函數+，-，*,/,string-append,not，我們可以直接寫：

(provide (rename-out [app #%app][datum #%datum] [add +][sub -][div /][mul *] [strapd string-append] [tnot not])) (define-syntax add (make-val-transformer (syntax-property #(lambda (x y) (+ x y)) type #(-> int int int))))(define-syntax sub (make-val-transformer (syntax-property #(lambda (x y) (- x y)) type #(-> int int int))))(define-syntax mul (make-val-transformer (syntax-property #(lambda (x y) (* x y)) type #(-> int int int))))(define-syntax div (make-val-transformer (syntax-property #(lambda (x y) (/ x y)) type #(-> int int int))))(define-syntax strapd (make-val-transformer (syntax-property #(lambda (x y) (string-append x y)) type #(-> string string string))))(define-syntax tnot (make-val-transformer (syntax-property #not type #(-> bool bool))))

對於上面這段冗餘的代碼，你也可以寫一個宏來簡化它們，不過，這不是本篇文章的目的。

接下來我們將會對app做一個檢查。

Type Check for app：

我們首先為app加上type check，檢查參數類型，並返回正確的類型。

(define-syntax (app stx) (syntax-case stx () [(_ func . args) (let ([types (map (lambda (x) (let ([t (syntax-property x type)]) (if t t (raise-syntax-error type-system-error "missing type:" x)))) (syntax->list #(func . args)))]) (syntax-property #(#%app func . args) type (type-app types)))]))

接下來定義type-app，它的行為遵循以下的規則。

type-app (-> a b) a=b

type-app (-> a b c ...) a rest ...=type-app (-> b c ...) rest ...

type-app other=error

補充：實際上這個type-app還寫的不夠好，但是我懶，你們饒了我把。

(define-for-syntax (type-app stx errorinf) (syntax-case stx () [((-> a b) c) (free-identifier=? a c) #b] [((-> a b c ...) d e ...) (free-identifier=? a d) (type-app #((-> b c ...) e ...) errorinf)] [others (raise-syntax-error type-system-error "error when apply the arguements to function" errofinf)]))

測試我們的程序，發現一個問題，它會提示我們已經支持的int，string，bool沒有類型，所以我們必須要對app進行修改,讓app的參數先展開（12.4 Syntax Transformers），才能獲取到參數的type。

(define-syntax (app stx) (syntax-case stx () [(_ func . args) (let ([types #`(#,@(map (lambda (x) (let ([t (syntax-property (local-expand x (syntax-local-context) (list ##%datum)) type)]) (if t t (raise-syntax-error type-system-error "missing type:" x)))) (syntax->list #(func . args))))]) (syntax-property #(#%app func . args) type (type-app types #(#%app func . args))))]))

這時，我們測試一下，發現各種運算都表現的很好，報錯也是正常的。

Type check for lambda：

下面我們要正式支持lambda了，先把lambda的form寫一下：

(lambda ([x : type] ...) expr)

大致思路是，將x的type代入expr中（make-val-transformer），然後根據獲得的type生成整個lambda term的type，好累。

(define-for-syntax (gen-type pa f) (syntax-case pa () [(a ...) #`(-> a ... #,f)] )) (define-syntax (lam stx) (syntax-case stx () [(_ ([var : types] ...) body) (let* ([body (local-expand #(lambda (var ...) (let-syntax ([var (make-val-transformer (syntax-property #var type #types))] ...) body)) (syntax-local-context) ())] [bodyt (syntax-case body () [(_ args (letvalues () (letvalues2 () e))) (syntax-property #e type)] [(_ (lam args (letvalues () (letvalues2 () e)))) (syntax-property #e type)] )] ) (if bodyt (syntax-property body type (gen-type #(types ...) bodyt)) (raise-syntax-error type-system-error "the body of lambda doesn;t have a type" #(lambda ([var : types] ...) body))) )]))

我們可以添加一個方便的語法形式print-type:來列印表達式的type：

(define-syntax (print-type: stx) (syntax-case stx () [(_ e) #`(begin (display #,(syntax-property (local-expand #e (syntax-local-context) ()) type)) (newline))]))

一些測試：

(require "type.rkt")((lambda ([x : int][y : int]) (* 1 (+ 4 x))) 2 3)((lambda ([x : string][y : string]) (string-append x y)) "dfd" "dfdf")(+ 1 2)(print-type: 3)(print-type: (not #t))(print-type: (lambda ([x : int] [y : string]) y))(print-type: (lambda ([x : int]) (lambda ([y : int]) x)))(print-type: (lambda ([x : int][y : int]) x))(print-type: +)result：6"dfddfdf"3intbool(-> int string string)(-> int (-> int int))(-> int int int)(-> int int int)

一點改進：

上面我們在判斷兩個類型是否相等時直接使用了非常naive的free-identifier=?，我們必須要改進它，採用把type全部展開後再逐個比較的方法。

(define-for-syntax (type=? x y) (or (and (identifier? x) (identifier? y) (free-identifier=? x y)) (and (stx-null? x) (stx-null? y)) (and (type=? (stx-car x) (stx-car y)) (type=? (stx-cdr x) (stx-cdr y)))))

最後，我們需要type-alias，比如

(define-type another-int int)

(define-type op (-> int int int))

甚至

(define-type (f3 t) (-> t t t))

看起來很複雜，其實我們根本不需要自己動手，只要借刀（宏）殺人就可以了。

為了防止type展開的時候出錯，我們需要先定義：

(define int type-int)(define string type-string)(define bool type-bool)(define -> (lambda l (error "ooh，you cant call me at runtime")))

然後把type=?中的參數用local-expand展開。

展開時我們會發現type-check無法通過，原因是->沒有type，我們可以把->單獨弄出來，而不是讓app進行check。

(define ->internal (lambda l (error "ooh")))(define-syntax -> (syntax-rules () [(_ a ...) (#%app ->internal a ...)]))

我們寫出不帶參數的define-type:

(define-syntax (define-type stx) (syntax-case stx () [(_ tname tvar) #(define-syntax tname (make-val-transformer #tvar))])

(print-type: (lambda ([x : another-int] [y : another-int]) (+ x y)))的結果是(-> another-int another-int int)，但是其實和(-> int int int)是一樣的。

如何實現(define-type (tc xx yy) e)這種形式，留給讀者自己動手實現。

由於我們的類型都是已經經過檢查的，所以根本不需要運行時檢查，可以把+的內部實現替換成unsafe-fx+，以此類推。

最後我們的type system還是不完善的，最好給speical form比如define（一般是core form）加上支持，不過這就留作讀者朋友的作業了。

另外，對於這種方法感興趣的同學，可以學習racket平台上的turnstile語言，只要寫出對應的typing rule，就可以輕易實現自己的類型系統啦。

附錄：全部源碼

#lang racket(require (for-syntax syntax/parse syntax/stx)) (require racket/unsafe/ops)(provide (rename-out [app #%app][datum #%datum] [add +][sub -][div /][mul *] [strapd string-append] [tnot not][lam lambda]))(provide print-type: int string bool -> define-type)(define int type-int)(define string type-string)(define bool type-bool)(define ->internal (lambda l (error "ooh,you cant call me at runtime")))(define-syntax -> (syntax-rules () [(_ a ...) (#%app ->internal a ...)]))(define-syntax (define-type stx) (syntax-case stx () [(_ tname tvar) #(define-syntax tname (make-val-transformer #tvar))] ))(define-for-syntax (type-app stx errorinf) (syntax-case stx () [((-> a b) c) (type=e? #a #c) #b] [((-> a b c ...) d e ...) (type=e? #a #d) (type-app #((-> b c ...) e ...) errorinf)] [others (raise-syntax-error type-system-error "error when apply the arguements to function" errorinf)]))(define-for-syntax (type=e? x y) (type=? (local-expand x (syntax-local-context) ()) (local-expand y (syntax-local-context) ())))(define-for-syntax (type=? x y) (or (and (identifier? x) (identifier? y) (free-identifier=? x y)) (and (stx-null? x) (stx-null? y)) (and (type=? (stx-car x) (stx-car y)) (type=? (stx-cdr x) (stx-cdr y)))))(define-syntax (app stx) (syntax-case stx () [(_ func . args) (let ([types #`(#,@(map (lambda (x) (let ([t (syntax-property (local-expand x (syntax-local-context) ()) type)]) (if t t (raise-syntax-error type-system-error "missing type:" x)))) (syntax->list #(func . args))))]) (syntax-property #(#%app func . args) type (type-app types #(#%app func . args))))]))(define-syntax (datum stx) (syntax-parse stx [(d . c:integer) (syntax-property #(#%datum . c) type #int)] [(d . c:boolean) (syntax-property #(#%datum . c) type #bool)] [(d . c:str) (syntax-property #(#%datum . c) type #string)] [(d . any) (raise-syntax-error type-system-error "Dont Support this type." #any)] ))(define-syntax (lam stx) (syntax-case stx () [(_ ([var : types] ...) body) (let* ([body (local-expand #(lambda (var ...) (let-syntax ([var (make-val-transformer (syntax-property #var type #types))] ...) body)) (syntax-local-context) ())] [bodyt (syntax-case body () [(_ args (letvalues () (letvalues2 () e))) (syntax-property #e type)] [(_ (lam args (letvalues () (letvalues2 () e)))) (syntax-property #e type)] )] ) (if bodyt (syntax-property body type (gen-type #(types ...) bodyt)) (raise-syntax-error type-system-error "the body of lambda doesn;t have a type" #(lambda ([var : types] ...) body))) )]))(define-syntax (print-type: stx) (syntax-case stx () [(_ e) #`(begin (display #,(syntax-property (local-expand #e (syntax-local-context) ()) type)) (newline))]))(define-for-syntax (gen-type pa f) (syntax-case pa () [(a ...) #`(-> a ... #,f)] )) (define-for-syntax (make-val-transformer val) (lambda (stx) (syntax-case stx () [_ (identifier? stx) val] [(_ . args) #`(app #,val . args)])))(define-syntax add (make-val-transformer (syntax-property #(lambda (x y) (unsafe-fx+ x y)) type #(-> int int int))))(define-syntax sub (make-val-transformer (syntax-property #(lambda (x y) (unsafe-fx- x y)) type #(-> int int int))))(define-syntax mul (make-val-transformer (syntax-property #(lambda (x y) (unsafe-fx* x y)) type #(-> int int int))))(define-syntax div (make-val-transformer (syntax-property #(lambda (x y) (unsafe-fx/ x y)) type #(-> int int int))))(define-syntax strapd (make-val-transformer (syntax-property #(lambda (x y) (string-append x y)) type #(-> string string string))))(define-syntax tnot (make-val-transformer (syntax-property #not type #(-> bool bool))))