turnstile/fomega2-tests passing

This commit is contained in:
Stephen Chang 2017-02-03 11:06:42 -05:00
parent 6e90aeaf18
commit 33c09db4d4
13 changed files with 433 additions and 119 deletions

View File

@ -17,7 +17,7 @@
(type-out ∀★ )
Λ inst tyλ tyapp)
(define-syntax-category :: kind :::)
(define-syntax-category :: kind)
; want #%type to be equiv to★
; => edit current-kind? so existing #%type annotations (with no #%kind tag)

View File

@ -20,7 +20,7 @@
λ #%app Λ inst
(for-syntax current-kind-eval kindcheck?))
(define-syntax-category :: kind :::)
(define-syntax-category :: kind)
;; modify predicates to recognize → (function type) as both type and kind
(begin-for-syntax
@ -40,7 +40,7 @@
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ)
#:with (τ- k_τ) (infer+erase #'τ)
#:with (τ- _) (infer+erase #'τ #:tag '::)
#'(define-syntax alias
(syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))

View File

@ -0,0 +1,34 @@
#lang s-exp macrotypes/typecheck
(extends "fomega.rkt" #:except tyapp tyλ)
;; NOTE 2017-02-03: currently not working
; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
; → is both type and kind --- but reuses parts of fomega.rkt,
; ie removes the duplication in fomega2.rkt
;; System F_omega
;; Type relation:
;; - redefine current-kind? and current-type so #%app and λ
;; work for both terms and types
;; Types:
;; - types from fomega.rkt
;; - String from stlc+reco+var
;; Terms:
;; - extend ∀ Λ inst from fomega.rkt
;; - #%datum from stlc+reco+var
;; types and kinds are now mixed, due to #%app and λ
(begin-for-syntax
(define old-kind? (current-kind?))
(current-kind? (λ (k) (or (#%type? k) (old-kind? k) (#%type? (typeof k)))))
;; Try to keep "type?" backward compatible with its uses so far,
;; eg in the definition of λ or previous type constuctors.
;; (However, this is not completely possible, eg define-type-alias)
;; So now "type?" no longer validates types, rather it's a subset.
;; But we no longer need type? to validate types, instead we can use
;; (kind? (typeof t))
(current-type? (λ (t) (or (type? t)
(let ([k (typeof t)])
(or (★? k) (∀★? k)))
((current-kind?) t)))))

View File

@ -1,6 +1,6 @@
#lang s-exp "../fomega2.rkt"
(require "rackunit-typechecking.rkt")
(require "rackunit-typechecking-fomega2.rkt")
(require "rackunit-kindchecking.rkt")
(check-kind Int :: )
(check-kind String :: )

View File

@ -0,0 +1,200 @@
#lang s-exp "../fomega3.rkt"
(require "rackunit-typechecking.rkt")
(check-type Int : )
(check-type String : )
(typecheck-fail )
(check-type ( Int Int) : )
(typecheck-fail ( ))
(typecheck-fail ( 1))
(check-type 1 : Int)
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type ( ([t : ]) ( t t)) : (∀★ ))
(check-type ( ( ([t : ]) ( t t)) ( Int Int)) : )
(check-type (Λ ([X : ]) (λ ([x : X]) x)) : ( ([X : ]) ( X X)))
(check-type ((λ ([x : ( ([X : ]) ( X X))]) x) (Λ ([X : ]) (λ ([x : X]) x)))
: ( ([X : ]) ( X X)))
(typecheck-fail ((λ ([x : ( ([X : ]) ( X X))]) x) (Λ ([X : ( )]) (λ ([x : X]) x))))
(check-type (λ ([t : ]) t) : ( ))
(check-type (λ ([t : ] [s : ]) t) : ( ))
(check-type (λ ([t : ]) (λ ([s : ]) t)) : ( ( )))
(check-type (λ ([t : ( )]) t) : ( ( ) ( )))
(check-type (λ ([t : ( )]) t) : ( ( ) ( )))
(check-type (λ ([arg : ] [res : ]) ( arg res)) : ( ))
(check-type ((λ ([t : ]) t) Int) : )
(check-type (λ ([x : ((λ ([t : ]) t) Int)]) x) : ( Int Int))
(check-type ((λ ([x : ((λ ([t : ]) t) Int)]) x) 1) : Int 1)
(check-type ((λ ([x : ((λ ([t : ]) t) Int)]) (+ x 1)) 1) : Int 2)
(check-type ((λ ([x : ((λ ([t : ]) t) Int)]) (+ 1 x)) 1) : Int 2)
(typecheck-fail ((λ ([x : ((λ ([t : ]) t) Int)]) (+ 1 x)) "a-string"))
;; partial-apply →
(check-type ((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int)
: ( ))
; f's type must have kind ★
(typecheck-fail (λ ([f : ((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int)]) f))
(check-type (Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f)) :
( ([tyf : ( )]) ( (tyf String) (tyf String))))
(check-type (inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int))
: ( ( Int String) ( Int String)))
(typecheck-fail
(inst (Λ ([X : ]) (λ ([x : X]) x)) 1))
;#:with-msg "not a valid type: 1")
;; applied f too early
(typecheck-fail (inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) (f 1)))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int)))
(check-type ((inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int))
(λ ([x : Int]) "int")) : ( Int String))
(check-type (((inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int))
(λ ([x : Int]) "int")) 1) : String "int")
;; tapl examples, p441
(typecheck-fail
(define-type-alias tmp 1))
;#:with-msg "not a valid type: 1")
(define-type-alias Id (λ ([X : ]) X))
(check-type (λ ([f : ( Int String)]) 1) : ( ( Int String) Int))
(check-type (λ ([f : ( Int String)]) 1) : ( ( Int (Id String)) Int))
(check-type (λ ([f : ( Int (Id String))]) 1) : ( ( Int String) Int))
(check-type (λ ([f : ( Int (Id String))]) 1) : ( ( Int (Id String)) Int))
(check-type (λ ([f : ( Int String)]) 1) : ( ( (Id Int) (Id String)) Int))
(check-type (λ ([f : ( Int String)]) 1) : ( ( (Id Int) String) Int))
(check-type (λ ([f : (Id ( Int String))]) 1) : ( ( Int String) Int))
(check-type (λ ([f : ( Int String)]) 1) : ( (Id ( Int String)) Int))
(check-type (λ ([f : (Id ( Int String))]) 1) : ( (Id ( Int String)) Int))
(check-type (λ ([f : (Id ( Int String))]) 1) : ( (Id (Id ( Int String))) Int))
;; tapl examples, p451
(define-type-alias Pair (λ ([A : ] [B : ]) ( ([X : ]) ( ( A B X) X))))
;(check-type Pair : (→ ★ ★ ★))
(check-type Pair : ( (∀★ )))
(check-type (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) x)) : ( ([X : ][Y : ]) ( X Y X)))
; parametric pair constructor
(check-type
(Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
: ( ([X : ][Y : ]) ( X Y (Pair X Y))))
; concrete Pair Int String constructor
(check-type
(inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String)
: ( Int String (Pair Int String)))
; Pair Int String value
(check-type
((inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String) 1 "1")
: (Pair Int String))
; fst: parametric
(check-type
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
: ( ([X : ][Y : ]) ( (Pair X Y) X)))
; fst: concrete Pair Int String accessor
(check-type
(inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
: ( (Pair Int String) Int))
; apply fst
(check-type
((inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
((inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String) 1 "1"))
: Int 1)
; snd
(check-type
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
: ( ([X : ][Y : ]) ( (Pair X Y) Y)))
(check-type
(inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
: ( (Pair Int String) String))
(check-type
((inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
((inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String) 1 "1"))
: String "1")
;;; sysf tests wont work, unless augmented with kinds
(check-type (Λ ([X : ]) (λ ([x : X]) x)) : ( ([X : ]) ( X X)))
(check-type (Λ ([X : ]) (λ ([t : X] [f : X]) t)) : ( ([X : ]) ( X X X))) ; true
(check-type (Λ ([X : ]) (λ ([t : X] [f : X]) f)) : ( ([X : ]) ( X X X))) ; false
(check-type (Λ ([X : ]) (λ ([t : X] [f : X]) f)) : ( ([Y : ]) ( Y Y Y))) ; false, alpha equiv
(check-type (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t1 : ]) ( ([t2 : ]) ( t1 ( t2 t2)))))
(check-type (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t3 : ]) ( ([t4 : ]) ( t3 ( t4 t4)))))
(check-not-type (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t4 : ]) ( ([t3 : ]) ( t3 ( t4 t4)))))
(check-type (inst (Λ ([t : ]) (λ ([x : t]) x)) Int) : ( Int Int))
(check-type (inst (Λ ([t : ]) 1) ( Int Int)) : Int)
; first inst should be discarded
(check-type (inst (inst (Λ ([t : ]) (Λ ([t : ]) (λ ([x : t]) x))) ( Int Int)) Int) : ( Int Int))
; second inst is discarded
(check-type (inst (inst (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) x))) Int) ( Int Int)) : ( Int Int))
;; polymorphic arguments
(check-type (Λ ([t : ]) (λ ([x : t]) x)) : ( ([t : ]) ( t t)))
(check-type (Λ ([t : ]) (λ ([x : t]) x)) : ( ([s : ]) ( s s)))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([s : ]) ( ([t : ]) ( t t))))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([r : ]) ( ([t : ]) ( t t))))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([r : ]) ( ([s : ]) ( s s))))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([r : ]) ( ([u : ]) ( u u))))
(check-type (λ ([x : ( ([t : ]) ( t t))]) x) : ( ( ([s : ]) ( s s)) ( ([u : ]) ( u u))))
(typecheck-fail ((λ ([x : ( (t) ( t t))]) x) (λ ([x : Int]) x)))
(typecheck-fail ((λ ([x : ( (t) ( t t))]) x) 1))
(check-type ((λ ([x : ( ([t : ]) ( t t))]) x) (Λ ([s : ]) (λ ([y : s]) y))) : ( ([u : ]) ( u u)))
(check-type
(inst ((λ ([x : ( ([t : ]) ( t t))]) x) (Λ ([s : ]) (λ ([y : s]) y))) Int) : ( Int Int))
(check-type
((inst ((λ ([x : ( ([t : ]) ( t t))]) x) (Λ ([s : ]) (λ ([y : s]) y))) Int) 10)
: Int 10)
(check-type (λ ([x : ( ([t : ]) ( t t))]) (inst x Int)) : ( ( ([t : ]) ( t t)) ( Int Int)))
(check-type (λ ([x : ( ([t : ]) ( t t))]) ((inst x Int) 10)) : ( ( ([t : ]) ( t t)) Int))
(check-type ((λ ([x : ( ([t : ]) ( t t))]) ((inst x Int) 10))
(Λ ([s : ]) (λ ([y : s]) y)))
: Int 10)
;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
(check-not-type 1 : ( Int Int))
;(typecheck-fail #f) ; unsupported literal
(check-type (λ ([x : Int] [y : Int]) x) : ( Int Int Int))
(check-not-type (λ ([x : Int]) x) : Int)
(check-type (λ ([x : Int]) x) : ( Int Int))
(check-type (λ ([f : ( Int Int)]) 1) : ( ( Int Int) Int))
(check-type ((λ ([x : Int]) x) 1) : Int 1)
(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
(check-type (λ ([f : ( Int Int Int)] [x : Int] [y : Int]) (f x y))
: ( ( Int Int Int) Int Int Int))
(check-type ((λ ([f : ( Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int 3)
(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
(typecheck-fail (λ ([x : ( Int Int)]) (+ x x))) ; x should be Int
(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int 20)

View File

@ -1,13 +1,15 @@
#lang info
(define compile-omit-paths
'("examples/tests"))
'("examples/fomega3.rkt"
"examples/tests"))
(define test-include-paths
'("examples/tests/mlish")) ; to include .mlish files
(define test-omit-paths
'("examples/tests/mlish/sweet-map.rkt" ; needs sweet-exp
"examples/tests/fomega3-tests.rkt"
"examples/tests/mlish/bg/README.md"))
(define test-timeouts

View File

@ -211,7 +211,10 @@
;; If Val is a non-empty list, return first element, otherwise return Val.
;; e.g., Stx = expression, Tag = ':, Val = Type stx
(define (detach stx tag)
(get-stx-prop/car stx tag)))
; (or
(get-stx-prop/car stx tag)
; (error 'detach "~a has no ~a prop" (stx->datum stx) tag))
))
;; ----------------------------------------------------------------------------
;; define-syntax-category ------------------------------------------------------

View File

@ -1,5 +1,5 @@
#lang turnstile/lang
(extends "sysf.rkt" #:except #%datum ~∀ ∀? Λ inst)
(extends "sysf.rkt" #:except #%datum ~∀ ∀? Λ inst λ #%app )
(reuse String #%datum #:from "stlc+reco+var.rkt")
; same as fomega.rkt except here λ and #%app works as both type and terms
@ -17,31 +17,42 @@
(provide define-type-alias
∀★
Λ inst)
λ #%app Λ inst
(for-syntax current-kind-eval kindcheck?))
(define-syntax-category kind)
(define-syntax-category :: kind)
(begin-for-syntax
(current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
(define old-kind? (current-kind?))
(current-kind? (λ (k) (or (#%type? k) (old-kind? k))))
;; Try to keep "type?" backward compatible with its uses so far,
;; eg in the definition of λ or previous type constuctors.
;; (However, this is not completely possible, eg define-type-alias)
;; So now "type?" no longer validates types, rather it's a subset.
;; But we no longer need type? to validate types, instead we can use
;; (kind? (typeof t))
(current-type? (λ (t) (or (type? t)
(let ([k (typeof t)])
(or (★? k) (∀★? k)))
((current-kind?) t)))))
(current-type? (λ (t) (define k (kindof t))
(and k ((current-kind?) k) (not (→? k)))))
;; o.w., a valid type is one with any valid kind
(current-any-type? (λ (t) (define k (kindof t))
(and k ((current-kind?) k)))))
; must override
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ)
#:with (τ- k_τ) (infer+erase #'τ)
#:with (τ- _) (infer+erase #'τ #:tag '::)
#'(define-syntax alias
(syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
;; extend → to serve as both type and kind
(define-syntax ( stx)
(syntax-parse stx
[(_ k:kind ...) ; kind
(add-orig (mk-kind #'(sysf:→- k.norm ...)) stx)]
[(_ . tys) #'(sysf:→ . tys)])) ; type
(define-base-kind )
(define-kind-constructor ∀★ #:arity >= 0)
(define-binding-type #:arr ∀★)
@ -73,28 +84,62 @@
(define old-type=? (current-type=?))
(define (type=? t1 t2)
(or (and (★? t1) (#%type? t2))
(and (#%type? t1) (★? t2))
(and (syntax-parse (list t1 t2) #:datum-literals (:)
[((~∀ ([tv1 : k1]) tbody1)
(~∀ ([tv2 : k2]) tbody2))
((current-type=?) #'k1 #'k2)]
[_ #t])
(old-type=? t1 t2))))
(syntax-parse (list t1 t2) #:datum-literals (:)
;; TODO: compare tbody1 and tbody2
[((~∀ ([tv1 : k1]) tbody1)
(~∀ ([tv2 : k2]) tbody2))
((current-kind=?) #'k1 #'k2)]
[_ (old-type=? t1 t2)]))
(current-type=? type=?)
(current=? type=?)
(current-typecheck-relation type=?)
(current-check-relation type=?))
(current-check-relation type=?)
(define old-kind=? (current-kind=?))
(define (new-kind=? k1 k2)
(or (and (★? k1) (#%type? k2)) ; enables use of existing type defs
(and (#%type? k1) (★? k2))
(old-kind=? k1 k2)))
(current-kind=? new-kind=?)
(current-kindcheck-relation new-kind=?))
(define-typed-syntax (Λ bvs:kind-ctx e)
[[bvs.x tv- : bvs.kind] ... e e- τ_e]
[[bvs.x tv- :: bvs.kind] ... e e- τ_e]
--------
[ e- ( ([tv- : bvs.kind] ...) τ_e)])
[ e- ( ([tv- :: bvs.kind] ...) τ_e)])
(define-typed-syntax (inst e τ ...)
[ e e- (~∀ (tv ...) τ_body) ( : (~∀★ k ...))]
[ τ τ- k] ...
(define-typed-syntax (inst e τ:any-type ...)
[ e e- (~∀ (tv ...) τ_body) ( :: (~∀★ k ...))]
#:do[(define old-check (current-check-relation))
(current-check-relation new-kind=?)]
[ τ τ- :: k] ...
#:do[(current-check-relation old-check)]
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
--------
[ e- τ-inst])
;; extend λ to also work as a type
;; must be define-typed-syntax because of default case
;; so use explicit tag in first case
(define-typed-syntax λ
[(_ bvs:kind-ctx τ) ; type
[[bvs.x X- :: bvs.kind] ... τ τ- :: k_res]
------------
[ (λ- (X- ...) τ-) :: ( bvs.kind ... k_res)]]
[(_ . rst)
--- [ (sysf:λ . rst)]]) ; term
;; extend #%app to also work as a type
(define-typed-syntax #%app
[(_ τ_fn τ_arg ...) ; type
[ τ_fn τ_fn- :: (~→ k_in ... k_out)]
#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
(num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
#:do[(define old-check (current-check-relation))
(current-check-relation new-kind=?)]
[ τ_arg τ_arg- :: k_in] ...
#:do[(current-check-relation old-check)]
-------------
[ (#%app- τ_fn- τ_arg- ...) :: k_out]]
[(_ . rst)
--- [ (sysf:#%app . rst)]]) ; term

View File

@ -1,74 +1,76 @@
#lang s-exp "../fomega2.rkt"
(require "rackunit-typechecking.rkt")
(require "rackunit-kindchecking.rkt")
(check-type Int : )
(check-type String : )
(check-kind Int :: )
(check-kind String :: )
(typecheck-fail )
(check-type ( Int Int) : )
(check-kind ( Int Int) :: )
(typecheck-fail ( ))
(typecheck-fail ( 1))
(check-type 1 : Int)
;; this should error but it doesnt
#;(λ ([x : ]) 1)
#;(λ ([x :: ]) 1)
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type ( ([t : ]) ( t t)) : (∀★ ))
(check-type ( ( ([t : ]) ( t t)) ( Int Int)) : )
;(check-type (∀ ([t :: ★]) (→ t t)) :: ★)
(check-kind ( ([t :: ]) ( t t)) :: (∀★ ))
(check-kind ( ( ([t :: ]) ( t t)) ( Int Int)) :: )
(check-type (Λ ([X : ]) (λ ([x : X]) x)) : ( ([X : ]) ( X X)))
(check-type (Λ ([X :: ]) (λ ([x : X]) x)) : ( ([X :: ]) ( X X)))
(check-type ((λ ([x : ( ([X : ]) ( X X))]) x) (Λ ([X : ]) (λ ([x : X]) x)))
: ( ([X : ]) ( X X)))
(typecheck-fail ((λ ([x : ( ([X : ]) ( X X))]) x) (Λ ([X : ( )]) (λ ([x : X]) x))))
(check-type ((λ ([x : ( ([X :: ]) ( X X))]) x) (Λ ([X :: ]) (λ ([x : X]) x)))
: ( ([X :: ]) ( X X)))
(typecheck-fail ((λ ([x : ( ([X :: ]) ( X X))]) x) (Λ ([X : ( )]) (λ ([x : X]) x))))
(check-type (λ ([t : ]) t) : ( ))
(check-type (λ ([t : ] [s : ]) t) : ( ))
(check-type (λ ([t : ]) (λ ([s : ]) t)) : ( ( )))
(check-type (λ ([t : ( )]) t) : ( ( ) ( )))
(check-type (λ ([t : ( )]) t) : ( ( ) ( )))
(check-type (λ ([arg : ] [res : ]) ( arg res)) : ( ))
;; tests for λ as a type
(check-kind (λ ([t :: ]) t) :: ( ))
(check-kind (λ ([t :: ] [s :: ]) t) :: ( ))
(check-kind (λ ([t :: ]) (λ ([s :: ]) t)) :: ( ( )))
(check-kind (λ ([t :: ( )]) t) :: ( ( ) ( )))
(check-kind (λ ([t :: ( )]) t) :: ( ( ) ( )))
(check-kind (λ ([arg :: ] [res :: ]) ( arg res)) :: ( ))
(check-type ((λ ([t : ]) t) Int) : )
(check-type (λ ([x : ((λ ([t : ]) t) Int)]) x) : ( Int Int))
(check-type ((λ ([x : ((λ ([t : ]) t) Int)]) x) 1) : Int 1)
(check-type ((λ ([x : ((λ ([t : ]) t) Int)]) (+ x 1)) 1) : Int 2)
(check-type ((λ ([x : ((λ ([t : ]) t) Int)]) (+ 1 x)) 1) : Int 2)
(typecheck-fail ((λ ([x : ((λ ([t : ]) t) Int)]) (+ 1 x)) "a-string"))
(check-kind ((λ ([t :: ]) t) Int) :: )
(check-type (λ ([x : ((λ ([t :: ]) t) Int)]) x) : ( Int Int))
(check-type ((λ ([x : ((λ ([t :: ]) t) Int)]) x) 1) : Int 1)
(check-type ((λ ([x : ((λ ([t :: ]) t) Int)]) (+ x 1)) 1) : Int 2)
(check-type ((λ ([x : ((λ ([t :: ]) t) Int)]) (+ 1 x)) 1) : Int 2)
(typecheck-fail ((λ ([x : ((λ ([t :: ]) t) Int)]) (+ 1 x)) "a-string"))
;; partial-apply →
(check-type ((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int)
: ( ))
(check-kind ((λ ([arg :: ]) (λ ([res :: ]) ( arg res))) Int)
:: ( ))
; f's type must have kind ★
(typecheck-fail (λ ([f : ((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int)]) f))
(check-type (Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f)) :
( ([tyf : ( )]) ( (tyf String) (tyf String))))
(typecheck-fail (λ ([f : ((λ ([arg :: ]) (λ ([res :: ]) ( arg res))) Int)]) f))
(check-type (Λ ([tyf :: ( )]) (λ ([f : (tyf String)]) f)) :
( ([tyf :: ( )]) ( (tyf String) (tyf String))))
(check-type (inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int))
(Λ ([tyf :: ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg :: ]) (λ ([res :: ]) ( arg res))) Int))
: ( ( Int String) ( Int String)))
(typecheck-fail
(inst (Λ ([X : ]) (λ ([x : X]) x)) 1))
;#:with-msg "not a valid type: 1")
(inst (Λ ([X :: ]) (λ ([x : X]) x)) 1)
#:with-msg "not a valid type: 1")
;; applied f too early
(typecheck-fail (inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) (f 1)))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int)))
(Λ ([tyf :: ( )]) (λ ([f : (tyf String)]) (f 1)))
((λ ([arg :: ]) (λ ([res :: ]) ( arg res))) Int)))
(check-type ((inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int))
(Λ ([tyf :: ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg :: ]) (λ ([res :: ]) ( arg res))) Int))
(λ ([x : Int]) "int")) : ( Int String))
(check-type (((inst
(Λ ([tyf : ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg : ]) (λ ([res : ]) ( arg res))) Int))
(Λ ([tyf :: ( )]) (λ ([f : (tyf String)]) f))
((λ ([arg :: ]) (λ ([res :: ]) ( arg res))) Int))
(λ ([x : Int]) "int")) 1) : String "int")
;; tapl examples, p441
(typecheck-fail
(define-type-alias tmp 1))
;#:with-msg "not a valid type: 1")
(define-type-alias Id (λ ([X : ]) X))
(define-type-alias Id (λ ([X :: ]) X))
(check-type (λ ([f : ( Int String)]) 1) : ( ( Int String) Int))
(check-type (λ ([f : ( Int String)]) 1) : ( ( Int (Id String)) Int))
(check-type (λ ([f : ( Int (Id String))]) 1) : ( ( Int String) Int))
@ -81,104 +83,104 @@
(check-type (λ ([f : (Id ( Int String))]) 1) : ( (Id (Id ( Int String))) Int))
;; tapl examples, p451
(define-type-alias Pair (λ ([A : ] [B : ]) ( ([X : ]) ( ( A B X) X))))
(define-type-alias Pair (λ ([A :: ] [B :: ]) ( ([X :: ]) ( ( A B X) X))))
;(check-type Pair : (→ ★ ★ ★))
(check-type Pair : ( (∀★ )))
;(check-type Pair :: (→ ★ ★ ★))
(check-type Pair :: ( (∀★ )))
(check-type (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) x)) : ( ([X : ][Y : ]) ( X Y X)))
(check-type (Λ ([X :: ] [Y :: ]) (λ ([x : X][y : Y]) x)) : ( ([X :: ][Y :: ]) ( X Y X)))
; parametric pair constructor
(check-type
(Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
: ( ([X : ][Y : ]) ( X Y (Pair X Y))))
(Λ ([X :: ] [Y :: ]) (λ ([x : X][y : Y]) (Λ ([R :: ]) (λ ([p : ( X Y R)]) (p x y)))))
: ( ([X :: ][Y :: ]) ( X Y (Pair X Y))))
; concrete Pair Int String constructor
(check-type
(inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
(inst (Λ ([X :: ] [Y :: ]) (λ ([x : X][y : Y]) (Λ ([R :: ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String)
: ( Int String (Pair Int String)))
; Pair Int String value
(check-type
((inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
((inst (Λ ([X :: ] [Y :: ]) (λ ([x : X][y : Y]) (Λ ([R :: ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String) 1 "1")
: (Pair Int String))
; fst: parametric
(check-type
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
: ( ([X : ][Y : ]) ( (Pair X Y) X)))
(Λ ([X :: ][Y :: ]) (λ ([p : ( ([R :: ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
: ( ([X :: ][Y :: ]) ( (Pair X Y) X)))
; fst: concrete Pair Int String accessor
(check-type
(inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
(Λ ([X :: ][Y :: ]) (λ ([p : ( ([R :: ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
: ( (Pair Int String) Int))
; apply fst
(check-type
((inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
(Λ ([X :: ][Y :: ]) (λ ([p : ( ([R :: ]) ( ( X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
Int String)
((inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
((inst (Λ ([X :: ] [Y :: ]) (λ ([x : X][y : Y]) (Λ ([R :: ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String) 1 "1"))
: Int 1)
; snd
(check-type
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
: ( ([X : ][Y : ]) ( (Pair X Y) Y)))
(Λ ([X :: ][Y :: ]) (λ ([p : ( ([R :: ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
: ( ([X :: ][Y :: ]) ( (Pair X Y) Y)))
(check-type
(inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
(Λ ([X :: ][Y :: ]) (λ ([p : ( ([R :: ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
: ( (Pair Int String) String))
(check-type
((inst
(Λ ([X : ][Y : ]) (λ ([p : ( ([R : ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
(Λ ([X :: ][Y :: ]) (λ ([p : ( ([R :: ]) ( ( X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
Int String)
((inst (Λ ([X : ] [Y : ]) (λ ([x : X][y : Y]) (Λ ([R : ]) (λ ([p : ( X Y R)]) (p x y)))))
((inst (Λ ([X :: ] [Y :: ]) (λ ([x : X][y : Y]) (Λ ([R :: ]) (λ ([p : ( X Y R)]) (p x y)))))
Int String) 1 "1"))
: String "1")
;;; sysf tests wont work, unless augmented with kinds
(check-type (Λ ([X : ]) (λ ([x : X]) x)) : ( ([X : ]) ( X X)))
;; sysf tests wont work, unless augmented with kinds
(check-type (Λ ([X :: ]) (λ ([x : X]) x)) : ( ([X :: ]) ( X X)))
(check-type (Λ ([X : ]) (λ ([t : X] [f : X]) t)) : ( ([X : ]) ( X X X))) ; true
(check-type (Λ ([X : ]) (λ ([t : X] [f : X]) f)) : ( ([X : ]) ( X X X))) ; false
(check-type (Λ ([X : ]) (λ ([t : X] [f : X]) f)) : ( ([Y : ]) ( Y Y Y))) ; false, alpha equiv
(check-type (Λ ([X :: ]) (λ ([t : X] [f : X]) t)) : ( ([X :: ]) ( X X X))) ; true
(check-type (Λ ([X :: ]) (λ ([t : X] [f : X]) f)) : ( ([X :: ]) ( X X X))) ; false
(check-type (Λ ([X :: ]) (λ ([t : X] [f : X]) f)) : ( ([Y :: ]) ( Y Y Y))) ; false, alpha equiv
(check-type (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t1 : ]) ( ([t2 : ]) ( t1 ( t2 t2)))))
(check-type (Λ ([t1 :: ]) (Λ ([t2 :: ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t1 :: ]) ( ([t2 :: ]) ( t1 ( t2 t2)))))
(check-type (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t3 : ]) ( ([t4 : ]) ( t3 ( t4 t4)))))
(check-type (Λ ([t1 :: ]) (Λ ([t2 :: ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t3 :: ]) ( ([t4 :: ]) ( t3 ( t4 t4)))))
(check-not-type (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t4 : ]) ( ([t3 : ]) ( t3 ( t4 t4)))))
(check-not-type (Λ ([t1 :: ]) (Λ ([t2 :: ]) (λ ([x : t1]) (λ ([y : t2]) y))))
: ( ([t4 :: ]) ( ([t3 :: ]) ( t3 ( t4 t4)))))
(check-type (inst (Λ ([t : ]) (λ ([x : t]) x)) Int) : ( Int Int))
(check-type (inst (Λ ([t : ]) 1) ( Int Int)) : Int)
(check-type (inst (Λ ([t :: ]) (λ ([x : t]) x)) Int) : ( Int Int))
(check-type (inst (Λ ([t :: ]) 1) ( Int Int)) : Int)
; first inst should be discarded
(check-type (inst (inst (Λ ([t : ]) (Λ ([t : ]) (λ ([x : t]) x))) ( Int Int)) Int) : ( Int Int))
(check-type (inst (inst (Λ ([t :: ]) (Λ ([t :: ]) (λ ([x : t]) x))) ( Int Int)) Int) : ( Int Int))
; second inst is discarded
(check-type (inst (inst (Λ ([t1 : ]) (Λ ([t2 : ]) (λ ([x : t1]) x))) Int) ( Int Int)) : ( Int Int))
(check-type (inst (inst (Λ ([t1 :: ]) (Λ ([t2 :: ]) (λ ([x : t1]) x))) Int) ( Int Int)) : ( Int Int))
;; polymorphic arguments
(check-type (Λ ([t : ]) (λ ([x : t]) x)) : ( ([t : ]) ( t t)))
(check-type (Λ ([t : ]) (λ ([x : t]) x)) : ( ([s : ]) ( s s)))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([s : ]) ( ([t : ]) ( t t))))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([r : ]) ( ([t : ]) ( t t))))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([r : ]) ( ([s : ]) ( s s))))
(check-type (Λ ([s : ]) (Λ ([t : ]) (λ ([x : t]) x))) : ( ([r : ]) ( ([u : ]) ( u u))))
(check-type (λ ([x : ( ([t : ]) ( t t))]) x) : ( ( ([s : ]) ( s s)) ( ([u : ]) ( u u))))
(check-type (Λ ([t :: ]) (λ ([x : t]) x)) : ( ([t :: ]) ( t t)))
(check-type (Λ ([t :: ]) (λ ([x : t]) x)) : ( ([s :: ]) ( s s)))
(check-type (Λ ([s :: ]) (Λ ([t :: ]) (λ ([x : t]) x))) : ( ([s :: ]) ( ([t :: ]) ( t t))))
(check-type (Λ ([s :: ]) (Λ ([t :: ]) (λ ([x : t]) x))) : ( ([r :: ]) ( ([t :: ]) ( t t))))
(check-type (Λ ([s :: ]) (Λ ([t :: ]) (λ ([x : t]) x))) : ( ([r :: ]) ( ([s :: ]) ( s s))))
(check-type (Λ ([s :: ]) (Λ ([t :: ]) (λ ([x : t]) x))) : ( ([r :: ]) ( ([u :: ]) ( u u))))
(check-type (λ ([x : ( ([t :: ]) ( t t))]) x) : ( ( ([s :: ]) ( s s)) ( ([u :: ]) ( u u))))
(typecheck-fail ((λ ([x : ( (t) ( t t))]) x) (λ ([x : Int]) x)))
(typecheck-fail ((λ ([x : ( (t) ( t t))]) x) 1))
(check-type ((λ ([x : ( ([t : ]) ( t t))]) x) (Λ ([s : ]) (λ ([y : s]) y))) : ( ([u : ]) ( u u)))
(check-type ((λ ([x : ( ([t :: ]) ( t t))]) x) (Λ ([s :: ]) (λ ([y : s]) y))) : ( ([u :: ]) ( u u)))
(check-type
(inst ((λ ([x : ( ([t : ]) ( t t))]) x) (Λ ([s : ]) (λ ([y : s]) y))) Int) : ( Int Int))
(inst ((λ ([x : ( ([t :: ]) ( t t))]) x) (Λ ([s :: ]) (λ ([y : s]) y))) Int) : ( Int Int))
(check-type
((inst ((λ ([x : ( ([t : ]) ( t t))]) x) (Λ ([s : ]) (λ ([y : s]) y))) Int) 10)
((inst ((λ ([x : ( ([t :: ]) ( t t))]) x) (Λ ([s :: ]) (λ ([y : s]) y))) Int) 10)
: Int 10)
(check-type (λ ([x : ( ([t : ]) ( t t))]) (inst x Int)) : ( ( ([t : ]) ( t t)) ( Int Int)))
(check-type (λ ([x : ( ([t : ]) ( t t))]) ((inst x Int) 10)) : ( ( ([t : ]) ( t t)) Int))
(check-type ((λ ([x : ( ([t : ]) ( t t))]) ((inst x Int) 10))
(Λ ([s : ]) (λ ([y : s]) y)))
(check-type (λ ([x : ( ([t :: ]) ( t t))]) (inst x Int)) : ( ( ([t :: ]) ( t t)) ( Int Int)))
(check-type (λ ([x : ( ([t :: ]) ( t t))]) ((inst x Int) 10)) : ( ( ([t :: ]) ( t t)) Int))
(check-type ((λ ([x : ( ([t :: ]) ( t t))]) ((inst x Int) 10))
(Λ ([s :: ]) (λ ([y : s]) y)))
: Int 10)

View File

@ -0,0 +1,26 @@
#lang racket/base
(require (for-syntax rackunit syntax/srcloc) rackunit macrotypes/typecheck
(only-in "../fomega2.rkt" current-kind-eval kindcheck?))
(provide check-kind)
(define-syntax (check-kind stx)
(syntax-parse stx #:datum-literals ( ->)
;; duplicate code to avoid redundant expansions
#;[(_ τ tag:id k-expected (~or ->) v)
#:with τ+ (expand/df #'(add-expected τ k-expected))
#:with k (detach #'e+ (stx->datum #'tag))
#:fail-unless (kindcheck? #'k ((current-kind-eval) #'k-expected))
(format
"Type ~a [loc ~a:~a] has kind ~a, expected ~a"
(syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ)
(type->str #'k) (type->str #'k-expected))
(syntax/loc stx (check-equal? τ+ (add-expected v k-expected)))]
[(_ τ tag:id k-expected)
#:with k (detach (expand/df #'(add-expected τ k-expected)) (stx->datum #'tag))
#:fail-unless
(kindcheck? #'k ((current-kind-eval) #'k-expected))
(format
"Type ~a [loc ~a:~a] has kind ~a, expected ~a"
(syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ)
(type->str #'k) (type->str #'k-expected))
#'(void)]))

View File

@ -120,7 +120,8 @@
((current-type=?) t1 #'t2*)]
[_ #f])))
(current-type=? new-type=?)
(current-typecheck-relation (current-type=?))
(current-typecheck-relation new-type=?)
(current-check-relation new-type=?)
;; current-type?
;; TODO: disabling type validation for now
@ -146,6 +147,7 @@
((current-type-eval) #'(CCs- a b c (Int (#%datum- . e-)))))]
[_ t+]))
(current-type-eval new-teval)
(current-ev new-teval)
;; type inference helpers ---------------------------------------------------
;; A "B" is a type binding, eg (X ty) or (ty X)

View File

@ -6,18 +6,18 @@
(define compile-omit-paths
'("examples/rosette"
"examples/tests"
"examples/trivial.rkt"))
"examples/fomega3.rkt"
"examples/trivial.rkt")) ; needs typed racket
(define test-include-paths
'("examples/tests/mlish")) ; to include .mlish files
(define test-omit-paths
'("examples/rosette"
"examples/tests/fomega2-tests.rkt"
"examples/tests/fomega3-tests.rkt"
"examples/tests/rosette" ; needs rosette
"examples/tests/trivial-test.rkt" ; needs typed/racket
"examples/tests/mlish/sweet-map.rkt" ; needs sweet-exp
"examples/tests/fomega3-tests.rkt"
"examples/tests/mlish/bg/README.md"))
(define test-timeouts