suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merged in occurrence (pull request #3)

Browse Source 
Occurrence Types: first draft
This commit is contained in:
stchang 2015-10-13 21:08:05 -04:00
commit 94b610c93b
2 changed files with 490 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

206
tapl/stlc+occurrence.rkt Normal file
View File

@ -0,0 +1,206 @@
#lang s-exp "typecheck.rkt"
(extends "stlc+sub.rkt" #:except #%datum)
;; Calculus for occurrence typing.
;; - Types can be simple, or sets of simple types
;; (aka "ambiguous types";
;; the run-time value will have one of a few ambiguous possible types.)
;; - The ∪ constructor makes ambiguous types
;; - `(test [τ ? x] e1 e2)` form will insert a run-time check to discriminate ∪
;; -- If the value at identifier x has type τ, then we continue to e1 with [x : τ]
;; -- Otherwise, we move to e2 with [x : (- (typeof x) τ)].
;; i.e., [x : τ] is not possible
;; - Subtyping rules:
;; -- ALL : t ... <: t' => (U t ...) <: t'
;; -- AMB : t <: (U ... t ...)
;; -- EXT : (U t' ...) <: (U t t' ...)
;; -- ONE : a<:b => (U a t' ...) <: (U b t' ...)
;; =============================================================================
(define-base-type Bot) ;; For empty unions
(define-base-type Boolean)
(define-base-type Str)
(define-typed-syntax #%datum
[(_ . n:boolean) (⊢ (#%datum . n) : Boolean)]
[(_ . n:str) (⊢ (#%datum . n) : Str)]
[(_ . x) #'(stlc+sub:#%datum . x)])
(define-type-constructor ∪ #:arity >= 1)
;; -----------------------------------------------------------------------------
;; --- Union operations
;; Occurrence type operations
;; These assume that τ is a type in 'normal form'
(begin-for-syntax
(define (∪->list τ)
;; Ignore type constructor & the kind
;; (because there are no bound identifiers)
(syntax-parse τ
[(~∪ τ* ...)
(syntax->list #'(τ* ...))]
[_
(error '∪->list (format "Given non-ambiguous type '~a'" τ))]))
(define (list->∪ τ*)
(if (null? τ*)
#'Bot
(τ-eval #`(∪ #,@τ*))))
(define (∖ τ1 τ2)
(cond
[(∪? τ1)
(define (not-τ2? τ)
(not (typecheck? τ τ2)))
(list->∪ (filter not-τ2? (∪->list τ1)))]
[else ; do nothing not non-union types
τ1]))
)
;; -----------------------------------------------------------------------------
;; --- Normal Form
;; Evaluate each type in the union,
;; remove duplicates
;; determinize the ordering of members
;; flatten nested unions
(begin-for-syntax
(define τ-eval (current-type-eval))
(define (τ->symbol τ)
;; TODO recurse for function types
(cadr (syntax->datum τ)))
(define (∪-eval τ-stx)
(syntax-parse (τ-eval τ-stx)
[(~∪ τ-stx* ...)
;; Recursively evaluate members
(define τ**
(for/list ([τ (in-list (syntax->list #'(τ-stx* ...)))])
(let ([τ+ (∪-eval τ)])
(if (∪? τ+)
(∪->list τ+)
(list τ+)))))
;; Remove duplicates from the union, sort members
(define τ*
(sort
(remove-duplicates (apply append τ**) (current-type=?))
symbol<?
#:key τ->symbol))
;; Check for empty & singleton lists
(define τ
(cond
[(null? τ*)
(raise-user-error 'τ-eval "~a (~a:~a) empty union type ~a\n"
(syntax-source τ-stx) (syntax-line τ-stx) (syntax-column τ-stx)
(syntax->datum τ-stx))]
[(null? (cdr τ*))
#`#,(car τ*)]
[else
#`#,(cons #'∪ τ*)]))
(τ-eval τ)]
[_
(τ-eval τ-stx)]))
(current-type-eval ∪-eval))
;; -----------------------------------------------------------------------------
;; --- Subtyping
(begin-for-syntax
;; True if one ordered list (of types) is a subset of another
(define (subset? x* y* #:leq [cmp (current-typecheck-relation)])
(let loop ([x* x*] [y* y*])
(cond
[(null? x*) #t]
[(null? y*) #f]
[(cmp (car x*) (car y*))
(loop (cdr x*) (cdr y*))]
[else
(loop x* (cdr y*))])))
(define sub? (current-sub?))
(define (∪-sub? τ1-stx τ2-stx)
(define τ1 ((current-type-eval) τ1-stx))
(define τ2 ((current-type-eval) τ2-stx))
(or (Bot? τ1) (Top? τ2)
(match `(,(∪? τ1) ,(∪? τ2))
['(#f #t)
;; AMB : a<:b => a <: (U ... b ...)
(for/or ([τ (in-list (∪->list τ2))])
(sub? τ1 τ))]
['(#t #t)
(define τ1* (∪->list τ1))
(define τ2* (∪->list τ2))
(match `(,(length τ1*) ,(length τ2*))
[`(,L1 ,L2) #:when (< L1 L2)
;; - EXT : (U t' ...) <: (U t t' ...)
(subset? τ1* τ2* #:leq sub?)]
[`(,L1 ,L2) #:when (= L1 L2)
;; - SUB : a<:b => (U a t' ...) <: (U b t' ...)
;; `∪->list` guarantees same order on type members
;; `sub?` is reflexive
(andmap sub? τ1* τ2*)]
[_ #f])]
['(#t #f)
;; - ALL : t... <: t' => (U t ...) <: t'
(andmap (lambda (τ) (sub? τ τ2)) (∪->list τ1))]
['(#f #f)
(sub? τ1 τ2)])))
(current-sub? ∪-sub?)
(current-typecheck-relation (current-sub?))
)
;; -----------------------------------------------------------------------------
;; --- Filters
;; These are stored imperatively, in a function.
;; Makes it easy to add a new filter & avoids duplicating this map
(begin-for-syntax
(define (simple-Π τ)
(syntax-parse (τ-eval τ)
[~Boolean
#'boolean?]
[~Int
#'integer?]
[~Str
#'string?]
[~Num
#'number?]
[~Nat
#'(lambda (n) (and (integer? n) (not (negative? n))))]
[_
(error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))]))
(define current-Π (make-parameter simple-Π)))
;; (test (τ ? x) e1 e2)
;; TODO:
;; - check if τ0 is a union type
;; - check if τ-filter is a subtype of τ0
;; - drop absurd branches?
;; - allow x not identifier (1. does nothing 2. latent filters)
(define-typed-syntax test #:datum-literals (?)
[(_ [τ-filter:type ? x-stx:id] e1 e2)
;; Get the filter type, evaluate to a runtime predicate
#:with f ((current-Π) #'τ-filter)
#:fail-unless (syntax-e #'f)
(format "Could not express type '~a' as a filter." #'τ-filter-stx)
;; TypeCheck e0:normally, e1:positive, e2:negative
#:with (x τ0) (infer+erase #'x-stx)
#:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ-filter]) #'e1)
#:with [x2 e2+ τ2] (infer/ctx+erase #`([x-stx : #,(∖ #'τ0 #'τ-filter)]) #'e2)
;; Expand to a conditional, using the runtime predicate
(⊢ (if (f x-stx)
((lambda x1 e1+) x-stx)
((lambda x2 e2+) x-stx))
: (∪ τ1 τ2))])
;; - TEST function filters (delayed filters?)
;; - disallow (U (-> ...) (-> ...))
;; - TEST latent filters -- listof BLAH
;; - integrate with sysf

284
tapl/tests/stlc+occurrence-tests.rkt Normal file
View File

@ -0,0 +1,284 @@
#lang s-exp "../stlc+occurrence.rkt"
(require "rackunit-typechecking.rkt")
;; -----------------------------------------------------------------------------
;; basic types & syntax
(check-type 1 : Int)
(check-type #f : Boolean)
(check-type "hello" : Str)
(check-type 1 : Top)
(check-type (λ ([x : (∪ Boolean Int)]) x)
: (→ (∪ Boolean Int) (∪ Boolean Int)))
(typecheck-fail
(λ ([x : ∪]) x)
#:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
(typecheck-fail
(λ ([x : (∪)]) x)
#:with-msg "Improper usage of type constructor ∪")
(typecheck-fail
(λ ([x : (∪ ∪)]) x)
#:with-msg "Improper usage of type constructor ∪")
(typecheck-fail
(λ ([x : (1 ∪)]) x)
#:with-msg "")
(typecheck-fail
(λ ([x : (Int ∪)]) x)
#:with-msg "expected identifier")
(typecheck-fail
(λ ([x : (→ ∪ ∪)]) x)
#:with-msg "Improper usage of type constructor ∪")
(typecheck-fail
(λ ([x : (→ Int ∪)]) x)
#:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
(typecheck-fail
(λ ([x : (∪ Int →)]) x)
#:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
;; -----------------------------------------------------------------------------
;; --- type evaluation
(check-type (λ ([x : (∪ Int Int Int Int)]) x)
: (→ Int Int))
(check-type (λ ([x : (∪ Int Boolean)]) 42)
: (→ (∪ Boolean Int) Int))
(check-type (λ ([x : (∪ Int Boolean Boolean Int)]) x)
: (→ (∪ Boolean Int) (∪ Boolean Int)))
(check-type (λ ([x : (∪ (∪ Int Boolean))]) 42)
: (→ (∪ Int Boolean) Int))
(check-type (λ ([x : (∪ Int Boolean)]) 42)
: (→ (∪ (∪ Int Boolean)) Int))
(check-type (λ ([x : (∪ Int Boolean)]) 42)
: (→ (∪ (∪ Int Boolean) (∪ Int Boolean)) Int))
;; -----------------------------------------------------------------------------
;; --- subtyping
;; ---- basics
(check-type 1 : (∪ Int))
(check-type 1 : (∪ (∪ Int)))
(check-type (λ ([x : Int]) x)
: (→ Bot Top))
(check-not-type 1 : (∪ Boolean))
;; - AMB : t <: t' => t <: (U ... t' ...)
(check-type 1 : (∪ Boolean Int))
(check-type -1 : (∪ Int Boolean))
(check-type 1 : (∪ Boolean Int (→ Boolean Boolean)))
(check-type 1 : (∪ (∪ Int Boolean) (∪ Int Boolean)))
(check-not-type 1 : (∪ Boolean (→ Int Int)))
;; --- EXT : (U t' ...) <: (U t t' ...)
(check-type (λ ([x : (∪ Int Boolean)]) x)
: (→ (∪ Int Boolean) (∪ Int Boolean Str)))
(check-type (λ ([x : (∪ Int Boolean)]) x)
: (→ (∪ Boolean) (∪ Int Boolean Str)))
(check-not-type (λ ([x : (∪ Int Boolean)]) x)
: (→ (∪ Int Boolean) (∪ Int)))
(check-not-type (λ ([x : (∪ Int Boolean)]) x)
: (→ (∪ Boolean Int Str) (∪ Int Boolean)))
;; --- SUB : a<:b => (U a t' ...) <: (U b t' ...)
(check-type (λ ([x : (∪ Int Str)]) x)
: (→ (∪ Int Str) (∪ Num Str)))
(check-type (λ ([x : (∪ Int Str)]) x)
: (→ (∪ Nat Str) (∪ Num Str)))
(check-type (λ ([x : (∪ Int Str)]) x)
: (→ (∪ Int Str) Top))
(check-not-type (λ ([x : (∪ Int Str)]) x)
: (→ Top (∪ Num Str)))
;; --- ALL
(check-type (λ ([x : (∪ Boolean Int Str)]) x)
: (→ (∪ Boolean Int Str) Top))
(check-type (λ ([x : (∪ Nat Int Num)]) x)
: (→ (∪ Nat Int Num) Num))
(check-type (λ ([x : (∪ Nat Int Num)]) x)
: (→ Nat Num))
;; --- misc
;; Because Int<:(U Int ...)
(check-type (λ ([x : (∪ Int Nat)]) #t)
: (→ Int Boolean))
;; -----------------------------------------------------------------------------
;; --- Basic Filters (applying functions)
;; --- is-boolean?
(check-type
(λ ([x : (∪ Boolean Int)])
(test [Boolean ? x]
#t
#f))
: (→ (∪ Boolean Int) Boolean))
(check-type-and-result
((λ ([x : (∪ Boolean Int)])
(test (Boolean ? x)
#t
#f)) #t)
: Boolean ⇒ #t)
(check-type-and-result
((λ ([x : (∪ Boolean Int)])
(test (Boolean ? x)
#t
#f)) 902)
: Boolean ⇒ #f)
;; --- successor
(check-type
(λ ([x : (∪ Int Boolean)])
(test (Int ? x)
(+ 1 x)
0))
: (→ (∪ Int Boolean) (∪ Num Nat)))
(check-type-and-result
((λ ([x : (∪ Int Boolean)])
(test (Int ? x)
(+ 1 x)
0)) #f)
: Num ⇒ 0)
(check-type-and-result
((λ ([x : (∪ Int Boolean)])
(test (Int ? x)
(+ 1 x)
1)) #t)
: Num ⇒ 1)
(check-type-and-result
((λ ([x : (∪ Int Boolean)])
(test (Int ? x)
(+ 1 x)
0)) 9000)
: Num ⇒ 9001)
;; ;; --- Do-nothing filter
(check-type
(λ ([x : Int])
(test (Int ? x) #t #f))
: (→ Int Boolean))
(check-type
(λ ([x : Int])
(test (Boolean ? x) 0 x))
: (→ Int (∪ Nat Int)))
;; --- Filter a subtype
(check-type
(λ ([x : (∪ Nat Boolean)])
(test (Int ? x)
x
x))
: (→ (∪ Nat Boolean) (∪ Int (∪ Nat Boolean))))
(check-type
(λ ([x : (∪ Int Boolean)])
(test (Nat ? x)
x
x))
: (→ (∪ Boolean Int) (∪ Int Nat Boolean)))
;; --- Filter a supertype
(check-type
(λ ([x : (∪ Int Boolean)])
(test (Num ? x)
1
x))
: (→ (∪ Boolean Int) (∪ Nat Boolean)))
(check-type-and-result
((λ ([x : (∪ Int Boolean)])
(test (Num ? x)
#f
x)) #t)
: Boolean
⇒ #t)
;; Should filter all the impossible types
(check-type-and-result
((λ ([x : (∪ Nat Int Num Boolean)])
(test (Num ? x)
#f
x)) #t)
: Boolean
⇒ #t)
;; -----------------------------------------------------------------------------
;; --- misc subtyping + filters (regression tests)
(check-type
(λ ([x : (∪ Int Boolean)])
(test (Int ? x)
0
1))
: (→ (∪ Int Boolean) Nat))
(check-type
(λ ([x : (∪ Int Boolean)])
(test (Int ? x)
0
1))
: (→ (∪ Int Boolean) Int))
;; -----------------------------------------------------------------------------
;; --- Invalid filters
(typecheck-fail
(λ ([x : (∪ Int Boolean)])
(test (1 ? x) #t #f))
#:with-msg "not a valid type")
(typecheck-fail
(test (1 ? 1) #t #f)
#:with-msg "not a valid type")
(typecheck-fail
(test (1 ? 1) #t #f)
#:with-msg "not a valid type")
(typecheck-fail
(test (#f ? #t) #t #f)
#:with-msg "not a valid type")
;; -----------------------------------------------------------------------------
;; --- Subtypes should not be collapsed
(check-not-type (λ ([x : (∪ Int Nat)]) #t)
: (→ Num Boolean))
(check-type ((λ ([x : (∪ Int Nat Boolean)])
(test (Int ? x)
2
(test (Nat ? x)
1
0)))
#t)
: Nat ⇒ 0)
(check-type ((λ ([x : (∪ Int Nat)])
(test (Nat ? x)
1
(test (Int ? x)
2
0)))
1)
: Nat ⇒ 1)
(check-type ((λ ([x : (∪ Int Nat)])
(test (Int ? x)
2
(test (Nat ? x)
1
0)))
-10)
: Nat ⇒ 2)
;; -----------------------------------------------------------------------------
;; --- TODO Filter values (should do nothing)
;; (check-type
;; (test (Int ? 1) #t #f)
;; : Boolean)
;; -----------------------------------------------------------------------------
;; --- TODO Filter functions
;; -----------------------------------------------------------------------------
;; --- TODO Latent filters (on data structures)