静的に型チェックするインタプリタ (EOPL の 4.1 と 4.2)

久しぶりに EOPL の練習問題に手をつけた。前回 3.7 節まで終わってたけど 3.8 と 3.9 はいったん飛ばして 4.1 と 4.2 の静的型チェックの導入をやることにした。

ここでは明示的に型を書かせて実行前に型チェックを行うのだけど let の左辺の変数の型なんかは推論する。明示的に書かないといけないのは関数の仮引数と再帰関数の戻り値の型のみ。そういえば Scala もそんな感じだ。

型チェックは「どの変数がどの型か」という情報を環境として持ちながら構文木をトラバースしていく。

型の記述の文法は EOPL だと proc (int x) のような C 風だったのだが、個人的な好みにより proc (x: int) のように変えた。

練習問題は代入式を追加したりタプルとリストのための構文を追加したりして、全部やった結果657行とずいぶんブログに貼るには長くなってしまった。テストケースを書けというのも練習問題にあって、書いたんだけどさすがにそれは貼らない。

タプルとリストの構文は新たな文法として追加する。プリミティブ関数として追加してはいけないのかなと最初思ったんだけど、この言語にはまだ総称性の概念が無いのでそうしてしまうとプリミティブ関数の型を表現する方法が無いことになる。

(load "r5rs.scm")
(load "define-datatype.scm")
(load "sllgen.scm")
(use srfi-1)

; representation of types
(define-datatype type type?
  (atomic-type
    (name symbol?))
  (proc-type
    (arg-types (list-of type?))
    (result-type type?))
  (pair-type
    (type1 type?)
    (type2 type?))
  (list-type
    (content-type type?))
  )

(define int-type (atomic-type 'int))
(define bool-type (atomic-type 'bool))

(define expand-type-expression
  (lambda (texp)
    (cases type-exp texp
      (int-type-exp () int-type)
      (bool-type-exp () bool-type)
      (proc-type-exp (arg-texps result-texp)
        (proc-type
          (expand-type-expressions arg-texps)
          (expand-type-expression result-texp)))
      (pair-type-exp (texp1 texp2)
        (pair-type
          (expand-type-expression texp1)
          (expand-type-expression texp2)))
      (list-type-exp (texp)
        (list-type
          (expand-type-expression texp)))
      )))

(define expand-type-expressions
  (lambda (texps)
    (map expand-type-expression texps)))

; checking for equal types
; Exercise 4.2 explicit recursive checking (instead of using equal?)
(define check-equal-type!
  (lambda (t1 t2 exp) ; exp is used only in the error message
    (let ((type-error
            (lambda ()
              (eopl:error 'check-equal-type!
                "Types didn't match: ~s != ~s in ~%~s"
                (type-to-external-form t1)
                (type-to-external-form t2)
                exp))))
      (letrec ((C-E-T!
              (lambda (t1 t2)
                (cases type t1
                  (atomic-type (name1)
                    (cases type t2
                      (atomic-type (name2)
                        (or (eqv? name1 name2) (type-error)))
                      (else (type-error))))
                  (proc-type (arg-types1 result-type1)
                    (cases type t2
                      (proc-type (arg-types2 result-type2)
                        (for-each
                          C-E-T!
                          (cons result-type1 arg-types1)
                          (cons result-type2 arg-types2)))
                      (else (type-error))))
                  (pair-type (t1-1 t1-2)
                    (cases type t2
                      (pair-type (t2-1 t2-2)
                        (begin
                          (C-E-T! t1-1 t2-1)
                          (C-E-T! t1-2 t2-2)))
                      (else (type-error))))
                  (list-type (content-type1)
                    (cases type t2
                      (list-type (content-type2)
                        (C-E-T! content-type1 content-type2))
                      (else (type-error))))
                  ))))
        (C-E-T! t1 t2)))))

(define type-to-external-form
  (lambda (ty)
    (cases type ty
      (atomic-type (name) name)
      (proc-type (arg-types result-type)
        (append
          (arg-types-to-external-form arg-types)
          '(->)
          (list (type-to-external-form result-type))))
      (pair-type (type1 type2)
        (list 'pairof
              (type-to-external-form type1)
              (type-to-external-form type2)))
      (list-type (content-type)
        (list 'list-of
              (type-to-external-form content-type)))
      )))

(define arg-types-to-external-form
  (lambda (arg-types)
    (cond
      ((null? arg-types) '())
      ((null? (cdr arg-types)) (list (type-to-external-form (car arg-types))))
      (else (cons (type-to-external-form (car arg-types))
                  (cons '* (arg-types-to-external-form (cdr arg-types))))))))

(define type-of-program
  (lambda (pgm)
    (cases program pgm
      (a-program (exp)
        (type-of-expression exp (empty-tenv))))))

(define type-of-expression
  (lambda (exp tenv)
    (cases expression exp
      (lit-exp (number) int-type)
      (true-exp () bool-type)
      (false-exp () bool-type)
      (var-exp (id) (apply-tenv tenv id))
      (if-exp (test-exp true-exp false-exp)
        (let ((test-type (type-of-expression test-exp tenv))
              (false-type (type-of-expression false-exp tenv))
              (true-type (type-of-expression true-exp tenv)))
          (check-equal-type! test-type bool-type test-exp)
          (check-equal-type! true-type false-type exp)
          true-type))
      (proc-exp (ids texps body)
        (type-of-proc-exp texps ids body tenv))
      (primapp-exp (prim rands)
        (type-of-application
          (type-of-primitive prim)
          (types-of-expressions rands tenv)
          prim rands exp))
      (app-exp (rator rands)
        (type-of-application
          (type-of-expression rator tenv)
          (types-of-expressions rands tenv)
          rator rands exp))
      (let-exp (ids rands body)
        (type-of-let-exp ids rands body tenv))
      (letrec-exp (proc-names idss texpss result-texps bodies letrec-body)
        (type-of-letrec-exp
          result-texps proc-names texpss idss bodies letrec-body tenv))
      (varassign-exp (id rhs-exp)
        (let ((var-type (apply-tenv tenv id))
              (exp-type (type-of-expression rhs-exp tenv)))
          (check-equal-type! var-type exp-type exp)
          int-type))
      (pair-exp (exp1 exp2)
        (pair-type
          (type-of-expression exp1 tenv)
          (type-of-expression exp2 tenv)))
      (unpack-exp (id1 id2 exp body)
        (let ((exp-type (type-of-expression exp tenv)))
          (cases type exp-type
            (pair-type (type1 type2)
              (let ((tenv-for-body
                      (extend-tenv
                        (list id1 id2)
                        (list type1 type2)
                        tenv)))
                (type-of-expression body tenv-for-body)))
            (else
              (eopl:error
                'type-of-expression
                "pair expected but got ~s"
                (type-to-external-form exp-type)
                )))))
      (list-exp (exps)
        (if (= 0 (length exps))
          (eopl:error
            'type-of-expression
            "At least 1 argument required in expression ~s"
            exp)
          (let ((t (type-of-expression (car exps) tenv)))
            (begin
              (for-each
                (lambda (x) (check-equal-type!
                              (type-of-expression x tenv)
                              t
                              exp))
                (cdr exps))
              (list-type t)))))
      (cons-exp (exp1 exp2)
        (let ((type2 (type-of-expression exp2 tenv)))
          (cases type type2
            (list-type (content-type)
              (begin
                (check-equal-type!
                  (type-of-expression exp1 tenv)
                  content-type
                  exp)
                type2))
            (else
              (eopl:error
                'type-of-expression
                "~s cannnot be cons'ed onto ~s"
                exp1 exp2)))))
      (null-exp (exp)
        (cases type (type-of-expression exp tenv)
          (list-type (content-type) bool-type)
          (else
            (eopl:error
              'type-of-expression
              "~s must be list type"
              exp))))
      (emptylist-exp (texp)
        (list-type (expand-type-expression texp)))
      (car-exp (exp)
        (let ((ty (type-of-expression exp tenv)))
          (cases type ty
            (list-type (content-type) content-type)
            (else
              (eopl:error
                'type-of-expression
                "~s must be list type" exp)))))
      (cdr-exp (exp)
        (let ((ty (type-of-expression exp tenv)))
          (cases type ty
            (list-type (content-type) ty)
            (else
              (eopl:error
                'type-of-expression
                "~s must be list type" exp)))))
      )))

(define types-of-expressions
  (lambda (rands tenv)
    (map (lambda (exp) (type-of-expression exp tenv)) rands)))

(define type-of-proc-exp
  (lambda (texps ids body tenv)
    (let ((arg-types (expand-type-expressions texps)))
      (let ((result-type
              (type-of-expression body
                (extend-tenv ids arg-types tenv))))
        (proc-type arg-types result-type)))))

(define type-of-application
  (lambda (rator-type rand-types rator rands exp)
    (cases type rator-type
      (proc-type (arg-types result-type)
        (if (= (length arg-types) (length rand-types))
          (begin
            (for-each
              check-equal-type!
              rand-types arg-types rands)
            result-type)
          (eopl:error 'type-of-expression
            (string-append
              "Wrong number of arguments in expression ~s:"
              "~%expected ~s~%got ~s")
            exp
            (map type-to-external-form arg-types)
            (map type-to-external-form rand-types))))
      (else
        (eopl:error 'type-of-expression
          "Rator not a proc type:~%~s~%had rator type ~s"
          rator (type-to-external-form rator-type))))))

; Exercise 4.3 list-structure parser for types
(define list-to-type
 (lambda (l)
    (cond
      ((symbol? l) (atomic-type l))
      ((list? l)
       (let ((len (length l)))
         (and (eqv? (list-ref l (- len 2)) '->)
              (proc-type
                (args-to-type (take l (- len 2)))
                (list-to-type (last l))))))
      (else eopl:error 'list-to-type ""))))
(define args-to-type
  (lambda (l)
    (cond
      ((null? l) '())
      ((null? (cdr l))
       (list (list-to-type (car l))))
      ((eqv? '* (cadr l))
       (cons (list-to-type (car l))
             (args-to-type (cddr l))))
      (else eopl:error 'list-to-type ""))))

(define type-of-primitive
  (lambda (prim)
    (cases primitive prim
      (add-prim ()
        (list-to-type '(int * int -> int)))
      (subtract-prim ()
        (list-to-type '(int * int -> int)))
      (mult-prim ()
        (list-to-type '(int * int -> int)))
      (incr-prim ()
        (list-to-type '(int -> int)))
      (decr-prim ()
        (list-to-type '(int -> int)))
      (zero?-prim ()
        (list-to-type '(int -> bool)))
      )))

(define type-of-let-exp
  (lambda (ids rands body tenv)
    (let ((tenv-for-body
            (extend-tenv
              ids
              (types-of-expressions rands tenv)
              tenv)))
      (type-of-expression body tenv-for-body))))

(define type-of-letrec-exp
  (lambda (result-texps proc-names texpss idss bodies letrec-body tenv)
    (let ((arg-typess
            (map
              (lambda (texps)
                (expand-type-expressions texps))
              texpss))
          (result-types
            (expand-type-expressions result-texps)))
      (let ((the-proc-types
              (map proc-type arg-typess result-types)))
        (let ((tenv-for-body
                (extend-tenv proc-names the-proc-types tenv)))
          (for-each
            (lambda (ids arg-types body result-type)
              (check-equal-type!
                (type-of-expression
                  body
                  (extend-tenv ids arg-types tenv-for-body))
                result-type
                body))
            idss arg-typess bodies result-types)
          (type-of-expression letrec-body tenv-for-body))))))

; boolean
(define true-value (lambda () #t))
(define false-value (lambda () #f))
(define true-value?
  (lambda (x)
    (not (eq? #f x))))

; reference
(define-datatype reference reference?
  (a-ref
    (position integer?)
    (vec vector?)))

(define primitive-deref
  (lambda (ref)
    (cases reference ref
      (a-ref (pos vec) (vector-ref vec pos)))))

(define primitive-setref!
  (lambda (ref val)
    (cases reference ref
      (a-ref (pos vec) (vector-set! vec pos val)))))

(define deref
  (lambda (ref)
    (primitive-deref ref)))

(define setref!
  (lambda (ref val)
    (primitive-setref! ref val)))

; environment
(define-datatype environment environment?
  (empty-env-record)
  (extended-env-record
    (syms (list-of symbol?))
    (vals vector?)
    (env environment?))
  )

(define empty-env
  (lambda ()
    (empty-env-record)))

(define extend-env
  (lambda (syms vals env)
    (extended-env-record syms (list->vector vals) env)))

(define extend-env-recursively
  (lambda (proc-names idss bodies old-env)
    (extended-env-record
      proc-names
      (list->vector
        (map
          (lambda (x) (closure x proc-names idss bodies old-env))
          (iota (length proc-names))))
      old-env)))

(define apply-env
  (lambda (env sym)
    (deref (apply-env-ref env sym))))

(define apply-env-ref
  (lambda (env sym)
    (cases environment env
      (empty-env-record ()
        (eopl:error 'apply-env "No binding for ~s" sym))
      (extended-env-record (syms vals env)
        (let ((pos (list-find-position sym syms)))
          (if (number? pos)
            (a-ref pos vals)
            (apply-env-ref env sym)))))))

(define list-find-position
  (lambda (sym los)
    (list-index (lambda (sym1) (eqv? sym1 sym)) los)))

(define list-index
  (lambda (pred ls)
    (cond
      ((null? ls) #f)
      ((pred (car ls)) 0)
      (else (let ((list-index-r (list-index pred (cdr ls))))
              (if (number? list-index-r)
                (+ list-index-r 1)
                #f))))))

; type environment
(define empty-tenv empty-env)
(define extend-tenv extend-env)
(define apply-tenv apply-env)

; procedure
(define-datatype procval procval?
  (closure
    (pos number?)
    (proc-names (list-of symbol?))
    (idss (list-of (list-of symbol?)))
    (bodies (list-of expression?))
    (env environment?)))

(define apply-procval
  (lambda (proc args)
    (cases procval proc
      (closure (pos proc-names idss bodies env)
        (eval-expression
          (list-ref bodies pos)
          (extend-env
            (list-ref idss pos)
            args
            (extend-env-recursively
              proc-names idss bodies env)))))))

; interpreter
(define eval-program
  (lambda (pgm)
    (cases program pgm
      (a-program (body)
        (eval-expression body (init-env))))))

(define eval-expression
  (lambda (exp env)
    (cases expression exp
      (lit-exp (datum) datum)
      (var-exp (id) (apply-env env id))
      (primapp-exp (prim rands)
        (let ((args (eval-rands rands env)))
          (apply-primitive prim args)))
      (if-exp (test-exp true-exp false-exp)
        (if (true-value? (eval-expression test-exp env))
          (eval-expression true-exp env)
          (eval-expression false-exp env)))
      (let-exp (ids rands body)
        (let ((args (eval-rands rands env)))
          (eval-expression body (extend-env ids args env))))
      (proc-exp (ids types body)
        (closure 0 (list '_) (list ids) (list body) env))
      (app-exp (rator rands)
        (let ((proc (eval-expression rator env))
              (args (eval-rands rands env)))
          (if (procval? proc)
            (apply-procval proc args)
            (eopl:error 'eval-expression
              "Attempt to apply non-procedure ~s" proc))))
      (letrec-exp (proc-names idss typess types bodies letrec-body)
        (eval-expression
          letrec-body
          (extend-env-recursively proc-names idss bodies env)))
      (varassign-exp (id rhs-exp)
        (begin
          (setref!
            (apply-env-ref env id)
            (eval-expression rhs-exp env))
          1))
      (pair-exp (exp1 exp2)
        (cons (eval-expression exp1 env)
              (eval-expression exp2 env)))
      (unpack-exp (id1 id2 exp body)
        (let ((pair (eval-expression exp env)))
          (eval-expression
            body
            (extend-env
              (list id1 id2)
              (list (car pair) (cdr pair))
              env))))
      (list-exp (exps)
        (eval-rands exps env))
      (cons-exp (exp1 exp2)
        (cons (eval-expression exp1 env)
              (eval-expression exp2 env)))
      (null-exp (exp)
        (null? (eval-expression exp env)))
      (emptylist-exp (texp)
        '())
      (car-exp (exp)
        (car (eval-expression exp env)))
      (cdr-exp (exp)
        (cdr (eval-expression exp env)))
      (true-exp  () #t)
      (false-exp () #f)
      )))

(define eval-rands
  (lambda (rands env)
    (map (lambda (x) (eval-rand x env)) rands)))

(define eval-rand
  (lambda (rand env)
    (eval-expression rand env)))

(define apply-primitive
  (lambda (prim args)
    (cases primitive prim
      (add-prim () (+ (car args) (cadr args)))
      (subtract-prim () (- (car args) (cadr args)))
      (mult-prim () (* (car args) (cadr args)))
      (incr-prim () (+ (car args) 1))
      (decr-prim () (- (car args) 1))
     ;(eq?-prim () (if (eq? (car args) (cadr args)) (true-value) (false-value)))
      (zero?-prim () (if (= (car args) 0) (true-value) (false-value)))
      )))

(define init-env (lambda () (empty-env)))

(define scanner-spec
  '((white-sp
      (whitespace) skip)
    (comment
      ("%" (arbno (not #\newline))) skip)
    (identifier
      (letter (arbno (or letter digit "?"))) symbol)
    (number
      (digit (arbno digit)) number)))

(define grammar
  '((program
      (expression)
      a-program)
    (expression
      (number)
      lit-exp)
    (expression
      (identifier)
      var-exp)
    (expression
      (primitive "(" (separated-list expression ",") ")" )
      primapp-exp)
    (expression
      ("if" expression "then" expression "else" expression)
      if-exp)
    (expression
      ("let" (arbno identifier "=" expression) "in" expression)
      let-exp)
    (expression
      ("proc" "(" (separated-list identifier ":" type-exp ",") ")" expression)
      proc-exp)
    (expression
      ("(" expression (arbno expression) ")")
      app-exp)
    (expression
      ("letrec"
       (arbno
         identifier
         "(" (separated-list identifier ":" type-exp  ",") ")"
         ":" type-exp
         "=" expression)
       "in" expression)
      letrec-exp)
    (expression
      ("set" identifier "=" expression)
      varassign-exp)
    (expression
      ("pair" "(" expression "," expression ")")
      pair-exp)
    (expression
      ("unpack" identifier identifier "=" expression "in" expression)
      unpack-exp)
    (expression
      ("list" "(" (separated-list expression ",") ")")
      list-exp)
    (expression
      ("cons" "(" expression "," expression ")")
       cons-exp)
    (expression
      ("null?" "(" expression ")")
      null-exp)
    (expression
      ("emptylist" "[" type-exp "]")
      emptylist-exp)
    (expression ("car" "(" expression ")") car-exp)
    (expression ("cdr" "(" expression ")") cdr-exp)
    (expression ("true") true-exp)
    (expression ("false") false-exp)
    (primitive ("+") add-prim)
    (primitive ("-") subtract-prim)
    (primitive ("*") mult-prim)
    (primitive ("add1") incr-prim)
    (primitive ("sub1") decr-prim)
   ;(primitive ("eq?") eq?-prim)
    (primitive ("zero?") zero?-prim)
    (type-exp ("int") int-type-exp)
    (type-exp ("bool") bool-type-exp)
    (type-exp
      ("(" (separated-list type-exp "*") "->" type-exp ")")
      proc-type-exp)
    (type-exp ("(pairof" type-exp type-exp ")") pair-type-exp)
    (type-exp ("(listof" type-exp ")") list-type-exp)
    ))

(define scan&parse
  (sllgen:make-string-parser
    scanner-spec
    grammar))

(sllgen:make-define-datatypes scanner-spec grammar)

(define run
  (lambda (string)
    (type-check string)
    (eval-program
      (scan&parse string))))

(define type-of
  (lambda (string)
    (type-of-program (scan&parse string))))

(define type-check
  (lambda (string)
    (type-to-external-form
      (type-of-program
        (scan&parse string)))))

(define read-eval-print
  (sllgen:make-rep-loop "-->" eval-program
    (sllgen:make-stream-parser
      scanner-spec
      grammar)))

タグ：EOPL