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

macrotypes/fomega2 tests passing

Browse Source
This commit is contained in:
Stephen Chang 2017-01-31 11:58:57 -05:00
parent e09e442c41
commit 03b6d6e713
7 changed files with 202 additions and 120 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
macrotypes/examples/fomega.rkt
View File

@ -1,5 +1,5 @@
#lang s-exp macrotypes/typecheck
(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
(extends "sysf.rkt" #:except #%datum ∀ ∀- ~∀ ∀? Λ inst)
(reuse String #%datum #:from "stlc+reco+var.rkt")
;; System F_omega

118
macrotypes/examples/fomega2.rkt
View File

@ -1,5 +1,5 @@
#lang s-exp macrotypes/typecheck
(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
@ -16,23 +16,25 @@
;; - #%datum from stlc+reco+var
(provide define-type-alias
★ ∀★ ∀
Λ inst)
★ ∀★ ∀ →
λ #%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
(current-kind? (λ (k) (or (#%type? k) (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)))))
(define old-kind? (current-kind?))
(current-kind? (λ (k) (or (#%type? k) (old-kind? k))))
;; well-formed types, eg not types with kind →
;; must allow kinds as types, for →
(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
@ -42,6 +44,13 @@
#'(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 ∀★)
@ -72,30 +81,71 @@
(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 (:)
[((~∀ ([tv1 : k1]) tbody1)
(~∀ ([tv2 : k2]) tbody2))
((current-kind=?) #'k1 #'k2)]
[_ (old-type=? t1 t2)]))
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
(current-typecheck-relation (current-type=?))
(define old-kind=? (current-kind=?))
(define (new-kind=? k1 k2)
(or (and (★? k1) (#%type? k2))
(and (#%type? k1) (★? k2))
(old-kind=? k1 k2)))
(current-kind=? new-kind=?)
(current-kindcheck-relation (current-kind=?)))
(define-typed-syntax Λ
[(_ bvs:kind-ctx e)
#:with ((tv- ...) e- τ_e)
(infer/ctx+erase #'bvs #'e)
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
(⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))])
(define-typed-syntax inst
[(_ e τ ...)
#:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
#:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
#:when (stx-andmap
(λ (t k) (or ((current-kind?) k)
(type-error #:src t #:msg "not a valid type: ~a" t)))
#'(τ ...) #'(k_τ ...))
#:when (typechecks? #'(k_τ ...) #'(k ...))
(⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))])
[(_ e τ:any-type ...)
; #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
#:with [e- τ_e] (infer+erase #'e)
#:with (~∀ (tv ...) τ_body) #'τ_e
#:with (~∀★ k ...) (kindof #'τ_e)
; #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
#:with (k_τ ...) (stx-map kindof #'(τ.norm ...))
#:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
(typecheck-fail-msg/multi
#'(k ...) #'(k_τ ...) #'(τ ...))
#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
(⊢ e- : τ_inst)])
;; extend λ to also work as a type
(define-typed-syntax λ
[(_ bvs:kind-ctx τ) ; type
#:with (Xs- τ- k_res) (infer/ctx+erase #'bvs #'τ #:tag '::)
(⊢ (λ- Xs- τ-) :: (→ bvs.kind ... k_res))]
[(_ . rst) #'(sysf:λ . rst)]) ; term
;; extend #%app to also work as a type
(define-typed-syntax #%app
[(_ τ_fn τ_arg ...) ; type
; #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
#:with [τ_fn- k_fn] (infer+erase #'τ_fn #:tag '::)
#:when (syntax-e #'k_fn) ; non-false
#:with (~→ k_in ... k_out ~!) #'k_fn
#:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:tag '::)
#:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...))
(string-append
(format
"~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
(syntax-source stx) (syntax-line stx) (syntax-column stx)
(syntax->datum #'τ_fn))
"or wrong number of arguments:\nGiven:\n"
(string-join
(map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
(syntax->datum #'(τ_arg ...))
(stx-map type->str #'(k_arg ...)))
"\n" #:after-last "\n")
(format "Expected: ~a arguments with type(s): "
(stx-length #'(k_in ...)))
(string-join (stx-map type->str #'(k_in ...)) ", "))
(⊢ (#%app- τ_fn- τ_arg- ...) :: k_out)]
[(_ . rst) #'(sysf:#%app . rst)]) ; term

167
macrotypes/examples/tests/fomega2-tests.rkt
View File

@ -1,10 +1,11 @@
#lang s-exp "../fomega2.rkt"
(require "rackunit-typechecking.rkt")
(require "rackunit-typechecking-fomega2.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)
@ -12,63 +13,64 @@
;; this should error but it doesnt
#;(λ ([x : ★]) 1)
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
;(check-kind (∀ ([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)) : (→ ★ ★ ★))
;; λ 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))
(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,105 @@
(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-kind 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)))
(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)

26
macrotypes/examples/tests/rackunit-typechecking-fomega2.rkt Normal file
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)]))

6
macrotypes/typecheck.rkt
View File

@ -54,7 +54,8 @@
[(_ . stuff)
(syntax/loc this-syntax
(#%module-begin
(provide #%module-begin #%top-interaction #%top require only-in) ; useful racket forms
; provide some useful racket forms
(provide #%module-begin #%top-interaction #%top require only-in)
. stuff))]))
(struct exn:fail:type:runtime exn:fail:user ())
@ -401,9 +402,10 @@
[(_ . ts)
#:with t-expanders (stx-map mk-~ #'ts)
#:with t?s (stx-map mk-? #'ts)
#:with t-s (filter identifier-binding (stx-map mk-- #'ts))
(expand-export
(syntax/loc stx (combine-out
(combine-out . ts)
(combine-out . ts) (combine-out . t-s)
(for-syntax (combine-out . t-expanders) . t?s)))
modes)]))))
(define-syntax define-base-type

2
turnstile/examples/fomega.rkt
View File

@ -1,5 +1,5 @@
#lang turnstile/lang
(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
(extends "sysf.rkt" #:except #%datum ∀ ∀- ~∀ ∀? Λ inst)
(reuse String #%datum #:from "stlc+reco+var.rkt")
;; System F_omega

1
turnstile/examples/tests/rackunit-typechecking.rkt
View File

@ -4,6 +4,7 @@
check-equal/rand
(rename-out [typecheck-fail check-stx-err]))
(begin-for-syntax
(define (add-esc s) (string-append "\\" s))
(define escs (map add-esc '("(" ")" "[" "]")))