diff --git a/Assignments/04.rkt b/Assignments/04.rkt index 51c7c73..ccfafae 100644 --- a/Assignments/04.rkt +++ b/Assignments/04.rkt @@ -27,7 +27,7 @@ [numT] [boolT] [arrowT (arg : Type) - (result : Type)] + (result : Type)] [objT (fields : (Hashof Symbol Type))]) (define-type-alias TypeEnv (Hashof Symbol Type)) @@ -51,10 +51,10 @@ [(arrowTE a b) (arrowT (interp-te a) (interp-te b))] [(objTE fields) (objT (hash - (map (lambda (key-val) - (values (fst key-val) - (interp-te (snd key-val)))) - fields)))])) + (map (lambda (key-val) + (values (fst key-val) + (interp-te (snd key-val)))) + fields)))])) (module+ test (test (interp-te (objTE (list (pair 'add1 (arrowTE (numTE) (numTE))) @@ -62,7 +62,37 @@ (objT (hash (list (pair 'add1 (arrowT (numT) (numT))) (pair 'compare (arrowT (numT) (boolT)))))))) -(define (subtype? X Y) ....) +(define (subtype? X Y) + (type-case Type X + [(numT) (type-case Type Y + [(numT) #t] + [else #f])] + [(boolT) (type-case Type Y + [(boolT) #t] + [else #f])] + [(arrowT X-arg X-result) + (type-case Type Y + [(arrowT Y-arg Y-result) + (and (subtype? Y-arg X-arg) ;; Contravariance of arguments + (subtype? X-result Y-result))] ;; Covariance of results + [else #f])] + [(objT X-fields) + (type-case Type Y + [(objT Y-fields) + (local [(define (loop keys) + (if (empty? keys) + #t + (let ([key (first keys)]) + (type-case (Optionof Type) (hash-ref Y-fields key) + [(none) #f] ;; Key not found in Y-fields + [(some Y-type) + (type-case (Optionof Type) (hash-ref X-fields key) + [(none) #f] ;; Key not found in X-fields + [(some X-type) + (and (subtype? X-type Y-type) ;; Check subtyping of field types + (loop (rest keys)))])]))))] ;; Recurse on remaining keys + (loop (hash-keys Y-fields)))] + [else #f])])) (module+ test (define hello-t (objT (hash (list (pair 'hello (numT)))))) @@ -78,14 +108,13 @@ (define (typecheck [exp : Exp] [env : TypeEnv]) : Type (local - [(define (num2 l r type) - (let ([left-t (typecheck l env)] - [right-t (typecheck r env)]) - (if (and (equal? (numT) left-t) (equal? (numT) right-t)) - type - (error 'typecheck "expected 2 num"))))] + [(define (num2 l r type) + (let ([left-t (typecheck l env)] + [right-t (typecheck r env)]) + (if (and (equal? (numT) left-t) (equal? (numT) right-t)) + type + (error 'typecheck "expected 2 num"))))] (type-case Exp exp - [(numE n) (numT)] [(boolE b) (boolT)] [(plusE l r) (num2 l r (numT))] @@ -140,12 +169,7 @@ [(some v) (typecheck v env)])] [(varE name) (type-case Type (type-lookup name env) - [(objT fields) - (type-case (Optionof Type) (hash-ref fields selector) - [(none) (error 'typecheck "unknown field")] - [(some v) (type-case Type v - [(arrowT arg-type result-type) v ] - [else v])])] + [(objT fields) (type-lookup selector fields)] [else (error 'typecheck "bound variable is not an object")])] [else (error 'typecheck "passing message to non-object")])]))) @@ -154,8 +178,7 @@ (module+ test (test/exn (parse `"strings are not in our language") "parse") - (test/exn (parse `{& 1 2}) "parse") -) + (test/exn (parse `{& 1 2}) "parse")) (define (sx-ref sx n) (list-ref (s-exp->list sx) n)) @@ -176,7 +199,7 @@ (define (parse sx) (local - [(define (px i) (parse (sx-ref sx i)))] + [(define (px i) (parse (sx-ref sx i)))] (cond [(s-exp-number? sx) (numE (s-exp->number sx))] [(s-exp-symbol? sx) @@ -232,9 +255,7 @@ (pair 'goodbye (numE 42))))) (test (parse `{lam {x : (obj (n-func (num -> num)))} x}) (lamE 'x (objTE (list (pair 'n-func (arrowTE (numTE) (numTE))))) - (varE 'x))) - - ) + (varE 'x)))) (tc : (S-Exp -> Type)) @@ -275,18 +296,31 @@ (test/exn (tc `{,obj-fun 2}) "argument type") (test/exn (tc `{if true ,obj-fun 2}) "branches") (test (tc `{rec {fact : (obj (run (num -> num)))} - {obj {run {lam {n : num} - {if {<= n 0} 1 {* n {{msg fact run} {- n 1}}}}}}} - {{msg fact run} 10}}) - (numT)) - - ) + {obj {run {lam {n : num} + {if {<= n 0} 1 {* n {{msg fact run} {- n 1}}}}}}} + {{msg fact run} 10}}) + (numT))) (module+ test - (test (tc `{,obj-fun {obj {n-func {lam {x : num} x}} - {b-func {lam {x : bool} x}}}}) (numT)) + (test (tc `{,obj-fun {obj {n-func {lam {x : num} x}} + {b-func {lam {x : bool} x}}}}) (numT)) - (test (tc `{let1 {f : {(obj (n-func (num -> num))) -> num}} - ,obj-fun - {f ,sampler}}) - (numT))) \ No newline at end of file + (test (tc `{let1 {f : {(obj (n-func (num -> num))) -> num}} + ,obj-fun + {f ,sampler}}) + (numT))) + +(module+ test + (test (subtype? (arrowT hello-t hello-t) + (arrowT hello-t hello-t)) #t) + (test (subtype? (arrowT hello-t hello-t) + (arrowT hello-t hello-goodbye-t)) #f) + (test (subtype? (arrowT hello-t hello-goodbye-t) + (arrowT hello-t hello-t)) #t) + (test (subtype? (arrowT hello-t hello-goodbye-t) + (arrowT hello-goodbye-t hello-t)) #t) + (test (subtype? (arrowT hello-goodbye-t hello-goodbye-t) + (arrowT hello-t hello-t)) #f) + ;; for coverage + (test (subtype? (arrowT (numT) (numT)) (numT)) #f) + (test (subtype? (numT) (arrowT (numT) (numT))) #f)) \ No newline at end of file