commit 5e1d3f1e223e99de0cc6d87b250f2b09ec9aa44e
parent e9a4a9f1dd4dd7e0d00c0af0ff9ff0f5cb014977
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 28 Mar 2016 17:11:38 -0400
mlish: suppot polymorphic recursion
Diffstat:
4 files changed, 96 insertions(+), 19 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -186,8 +186,8 @@
(stlc+rec-iso:define-type-alias Name Name2))]
[(_ (Name:id X:id ...)
;; constructors must have the form (Cons τ ...)
- ;; but the first ~or clause accepts 0-arg constructors as ids
- ;; the ~and is required to bind the duplicate Cons ids (see Ryan's email)
+ ;; but the first ~or clause accepts 0-arg constructors as ids;
+ ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email)
(~and (~or (~and IdCons:id
(~parse (Cons [fld (~datum :) τ] ...) #'(IdCons)))
(Cons [fld (~datum :) τ] ...)
@@ -199,20 +199,29 @@
#:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
-; #:with ((fld ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
#'(StructName ...) #'((fld ...) ...))
#:with (Cons? ...) (stx-map mk-? #'(StructName ...))
#:with get-Name-info (format-id #'Name "get-~a-info" #'Name)
;; types, but using RecName instead of Name
- #:with ((τ/rec ...) ...) (subst-expr #'RecName #'(Name X ...) #'((τ ...) ...))
+ #:with ((τ/rec ...) ...) (subst #'RecName #'Name #'((τ ...) ...))
#`(begin
(define-type-constructor Name
#:arity = #,(stx-length #'(X ...))
#:extra-info (X ...)
(λ (RecName)
- (let-syntax ([RecName (make-rename-transformer
- (assign-type #'RecName #'#%type))])
+ (let-syntax
+ ([RecName
+ (syntax-parser
+ [(_ . rst)
+ ;; - this is a placeholder to break the recursion
+ ;; - clients, like match, must manually unfold by
+ ;; replacing the entire (#%plain-app RecName ...) stx
+ ;; - to preserve polymorphic recursion, the entire stx
+ ;; should be replaced but with #'rst as the args
+ ;; in place of args in the input type
+ ;; (see subst-special in typecheck.rkt)
+ (assign-type #'(#%plain-app RecName . rst) #'#%type)])])
('Cons Cons? [acc τ/rec] ...) ...))
#:no-provide)
(struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
@@ -291,6 +300,7 @@
;; match --------------------------------------------------
(define-syntax (match stx)
(syntax-parse stx #:datum-literals (with ->)
+ ;; TODO: eliminate redundant expansions
[(_ e with . clauses)
;; e is tuple
#:with [e- ty_e] (infer+erase #'e)
@@ -320,7 +330,7 @@
((~literal let-values) ()
. info-body)))
(get-extra-info #'τ_e)
- #:with info-unfolded (subst #'τ_e #'RecName #'info-body)
+ #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
#:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
#:fail-unless (set=? (syntax->datum #'(Clause ...))
(syntax->datum #'(ConsAll ...)))
@@ -341,6 +351,7 @@
(equal? Cl (syntax->datum #'C))])
#'info-unfolded))
(syntax->datum #'(Clause ...)))
+ ;; this commented block experiments with expanding to unsafe ops
;; #:with ((acc ...) ...) (stx-map
;; (lambda (accs)
;; (for/list ([(a i) (in-indexed (syntax->list accs))])
diff --git a/tapl/tests/mlish/polyrecur.mlish b/tapl/tests/mlish/polyrecur.mlish
@@ -0,0 +1,28 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; tests of polymorphic recursion
+
+;; polymorphic recursion of functions
+(define (polyf [lst : (List X)] -> (List X))
+ (let ([x (polyf (list 1 2 3))]
+ [y (polyf (list #t #f))])
+ (polyf lst)))
+
+;; polymorphic recursive type
+;; from okasaki, ch10
+(define-type (Seq X)
+ Nil
+ (Cons X (Seq (× X X))))
+
+(define (size [s : (Seq X)] -> Int)
+ (match s with
+ [Nil -> 0]
+ [Cons x ps -> (add1 (* 2 (size ps)))]))
+
+(check-type (size (Nil {Int})) : Int -> 0)
+(check-type (size (Cons 1 Nil)) : Int -> 1)
+(check-type (size (Cons 1 (Cons (tup 2 3) Nil))) : Int -> 3)
+(check-type
+ (size (Cons 1 (Cons (tup 2 3) (Cons (tup (tup 4 5) (tup 6 7)) Nil))))
+ : Int -> 7)
diff --git a/tapl/tests/run-all-mlish-tests.rkt b/tapl/tests/run-all-mlish-tests.rkt
@@ -25,3 +25,6 @@
(require "mlish/bg/basics.mlish")
(require "mlish/bg/huffman.mlish")
(require "mlish/bg/lambda.rkt")
+
+;; okasaki, polymorphic recursion
+(require "mlish/polyrecur.mlish")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -422,13 +422,22 @@
(define (brace? stx)
(define paren-shape/#f (syntax-property stx 'paren-shape))
(and paren-shape/#f (char=? paren-shape/#f #\{)))
+ ;; todo: abstract out the common shape of a type constructor,
+ ;; i.e., the repeated pattern code in the functions below
(define (get-extra-info t)
(syntax-parse t
[((~literal #%plain-app) internal-id
((~literal #%plain-lambda) bvs
((~literal #%expression) extra-info-to-extract) . rst))
#'extra-info-to-extract]
- [_ #'void])))
+ [_ #'void]))
+ (define (get-tyargs ty)
+ (syntax-parse ty
+ [((~literal #%plain-app) internal-id
+ ((~literal #%plain-lambda) bvs
+ xtra-info . rst))
+ #'rst])))
+
(define-syntax define-basic-checked-id-stx
(syntax-parser #:datum-literals (:)
@@ -693,16 +702,8 @@
stx))
; subst τ for y in e, if (bound-id=? x y)
(define (subst τ x e)
- #'(printf "subst ~a for ~a in ~a\n"
- (syntax->datum τ)
- x
- (syntax->datum e))
(syntax-parse e
[y:id #:when (bound-identifier=? e x)
- ; #:when (printf "~a = ~a\n" #'y x)
-; #:when
-; (displayln (syntax-property (syntax-track-origin τ #'y #'y) 'type))
-; #:when (displayln (syntax-property (syntax-property (syntax-track-origin τ #'y #'y) 'type #'#%type) 'type))
; use syntax-track-origin to transfer 'orig
; but may transfer multiple #%type tags, so merge
(merge-type-tags (syntax-track-origin τ #'y #'y))]
@@ -714,11 +715,24 @@
(define (substs τs xs e)
(stx-fold subst e τs xs))
- ;; subst-expr
- ;; used for inferring recursive types
+ ;; subst-expr:
+ ;; - like subst except the target can be any stx, rather than just an id
+ ;; - used for implementing polymorphic recursive types
+ (define (stx-lam? s)
+ (syntax-parse s
+ [((~literal #%plain-lambda) . rst) #t] [_ #f]))
+ (define (stx-lam=? s1 s2)
+ (syntax-parse (list s1 s2)
+ [(((~literal #%plain-lambda) xs . bs1)
+ ((~literal #%plain-lambda) ys . bs2))
+ #:with zs (generate-temporaries #'xs)
+ (and (stx-length=? #'xs #'ys)
+ (stx=? (substs #'zs #'xs #'bs1)
+ (substs #'zs #'ys #'bs2)))]))
(define (stx=? s1 s2)
(or (and (identifier? s1) (identifier? s2) (free-identifier=? s1 s2))
(and (stx-null? s1) (stx-null? s2))
+ (and (stx-lam? s1) (stx-lam? s2) (stx-lam=? s1 s2))
(and (stx-pair? s1) (stx-pair? s2) (stx-length=? s1 s2)
(stx-andmap stx=? s1 s2))))
;; subst e1 for e2 in e3
@@ -727,5 +741,26 @@
[(stx=? e2 e3) e1]
[(identifier? e3) e3]
[else ; stx-pair
- (stx-map (lambda (e) (subst-expr e1 e2 e)) e3)]))
+ (with-syntax ([result (stx-map (lambda (e) (subst-expr e1 e2 e)) e3)])
+ (syntax-track-origin #'result e3 #'here))]))
+ (define (subst-exprs τs xs e)
+ (stx-fold subst-expr e τs xs))
+ ;; subst-special:
+ ;; - used for unfolding polymorphic recursive type
+ ;; subst ty1 for x in ty2
+ ;; where ty1 is an applied type constructor type
+ ;; x is a placeholder for an applied tycons type in ty2
+ ;; - subst special first replaces the args of ty1 with that of x
+ ;; before replacing applications of tycons x with this modified ty1
+ (define (subst-special ty1 x ty2)
+ (cond
+ [(identifier? ty2) ty2]
+ [(syntax-parse ty2 [((~literal #%plain-app) tycons:id . _) (free-identifier=? #'tycons x)] [_ #f])
+ (syntax-parse ty2
+ [((~literal #%plain-app) tycons:id . newargs)
+; #:with oldargs (get-tyargs ty1)
+ (subst-exprs #'newargs (get-tyargs ty1) ty1)])]
+ [else ; stx-pair
+ (with-syntax ([result (stx-map (lambda (e) (subst-special ty1 x e)) ty2)])
+ (syntax-track-origin #'result ty2 #'here))]))
)
