www

commit 050c43b3a2eea7fc53f17219970b633799059b8d
parent 0aa2857e7442be0570520edccc73d68d3b44573e
Author: Ben Greenman <types@ccs.neu.edu>
Date:   Tue,  6 Oct 2015 16:32:26 -0400

[occurrence] constructor + basic tests

Diffstat:
A
tapl/stlc+occurrence.rkt
 | 
38
++++++++++++++++++++++++++++++++++++++
A
tapl/tests/stlc+occurrence-tests.rkt
 | 
50
++++++++++++++++++++++++++++++++++++++++++++++++++

2 files changed, 88 insertions(+), 0 deletions(-)
diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
@@ -0,0 +1,38 @@
+#lang s-exp "typecheck.rkt"
+(extends "stlc+sub.rkt" #:except #%datum)
+;; TODO import if- form?
+
+;; Calculus for occurrence typing.
+;; - Types can be simple, or sets of simple types
+;;   (aka "ambiguous types".
+;;    The type is one of a few ambiguous possibilities at compile-time)
+;; - The U constructor makes ambiguous types
+;; - `(if-τ? [x : τ] e1 e2)` form will insert a run-time check to discriminate amb. types
+;; - For non-top types, τ is a subtype of (∪ τ1 ... τ τ2 ...)
+
+;; =============================================================================
+
+(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)
+
+;; - define normal form for U, sorted
+;; - TEST create U types
+;; - subtype U with simple, U with contained
+;; - TEST subtyping, with 'values' and with 'functions'
+;; - add filters
+;; - TEST basic filters
+;; - TEST function filters (delayed filters?)
+;; - disallow (U (-> ...) (-> ...))
+;; - TEST latent filters -- listof BLAH
+;; - integrate with sysf
+
+;; (begin-for-syntax
+;;   (define stlc:sub? (current-sub?))
+;; )
diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt
@@ -0,0 +1,50 @@
+#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)))
+(check-type (λ ([x : (∪ Int Int Int Int)]) x)
+            : (→ (∪ Int Int Int Int) (∪ Int Int Int 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 ∪: ∪, expected >= 1 arguments")
+(typecheck-fail
+ (λ ([x : (1 ∪)]) x)
+ ;; TODO Weird message for this one.
+ #:with-msg "Expected expression 1 to have → type")
+(typecheck-fail
+ (λ ([x : (Int ∪)]) x)
+ ;; TODO a little weird of a message
+ #:with-msg "expected identifier")
+(typecheck-fail
+ (λ ([x : (→ ∪ ∪)]) 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")
+(typecheck-fail
+ (λ ([x : (∪ Int →)]) x)
+ #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
+
+;; (check-type 1 : (∪ Int))
+;; (check-type 1 : (∪ Int Boolean))
+;; (check-type 1 : (∪ Boolean Int))
+;; (check-type 1 : (∪ Boolean Int (→ Boolean Boolean)))
+;; (check-type 1 : (∪ (∪ Int)))
+
+;; (check-not-type 1 : (∪ Boolean))
+;; (check-not-type 1 : (∪ Boolean (→ Int Int)))