NOTE: represent type by s-exp when doing inference


Programming Language Theory • System Programming

NOTE: represent type by s-exp when doing inference

Compare with old implementation, this version improves by using s-exp to represent type, therefore, can reduce unify size a lot.

(define (lookup/type-of env v)
  (hash-ref env v))
(define (extend/env env v t)
  (hash-set env v t))

(define (occurs v t)
  (match t
    [`(,t* ...)
     (ormap (λ (t) (occurs v t)) t*)]
    [t (equal? v t)]))

(define (unify t1 t2)
  (match* (t1 t2)
    [(_ t2) #:when (parameter? t2)
            (if (or (eqv? t1 (t2)) (not (occurs (t2) t1)))
                (t2 t1)
                (error (format "~a occurs in ~a" (t2) t1)))]
    [(t1 _) #:when (parameter? t1)
            (unify t2 t1)]
    [(`(,a* ...) `(,b* ...))
     (for-each unify a* b*)]
    [(_ _)
     (unless (eqv? t1 t2)
       (error (format "cannot unify type ~a and ~a" t1 t2)))]))

(define (recur-infer tm [env (make-immutable-hash)])
  (match tm
    [`(λ (,x* ...) ,t)
     (let ([λ-env (foldl (λ (x e)
                           (extend/env e x (make-parameter (gensym))))
                         env x*)])
       `(-> ,(map (λ (x) (lookup/type-of λ-env x)) x*)
            ,(recur-infer t λ-env)))]
    [`(let ([,x* ,xt*] ...) ,t)
     (let ([let-env (foldl (λ (x t e)
                             ; use GEN for each binding
                             ; INST for each variable occurs
                             (extend/env e x (recur-infer t e)))
                           env x* xt*)])
       (recur-infer t let-env))]
    [`(quote ,p*)
     `(list ,(if (empty? p*)
                 (make-parameter (gensym))
                 (let ([et (recur-infer (car p*) env)])
                   (for-each (λ (et*) (unify et* et))
                             (map (λ (x) (recur-infer x env)) (cdr p*)))
    [`(,f ,arg* ...)
     (let ([free (make-parameter (gensym))])
       (unify (recur-infer f env)
              `(-> ,(map (λ (arg) (recur-infer arg env)) arg*) ,free))
    [x (cond
         [(string? x) 'string]
         [(number? x) 'number]
         [(char? x) 'char]
         [(symbol? x) (lookup/type-of env x)]
         [else (error (format "unknown form: ~a" x))])]))

(define (elim-free ty)
  (match ty
    [`(,ty* ...)
     (map elim-free ty*)]
    [ty (if (parameter? ty)
            (elim-free (ty))

(define (infer tm) (elim-free (recur-infer tm)))

author: Lîm Tsú-thuàn/林子篆/Danny


tag:noteplthindley milnerracket

Similar Articles

Buy Me A CoffeeCreative Commons Attribution-NonCommercial-NoDerivatives 4.0 InternationalAll works in this site is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
©2021 dannypsnl(林子篆)