use :: key in turnstile/fomega-no-reuse; simplify turnstile/fomega
This commit is contained in:
Stephen Chang
parent
33c09db4d4
commit
eb2e012e9d
179
turnstile/examples/fomega-no-reuse-old.rkt
Normal file
179
turnstile/examples/fomega-no-reuse-old.rkt
Normal file
|
|
@ -0,0 +1,179 @@
|
|||
#lang turnstile/lang
|
||||
|
||||
;; System F_omega, without reusing rules from other languages
|
||||
;; - try to avoid using built-in "kind" system (ie #%type)
|
||||
;; - not quite there: define-primop and typed-out still use current-type?
|
||||
;; - use define-internal- forms instead
|
||||
|
||||
;; example suggested by Alexis King
|
||||
|
||||
;; this version still uses ': key for kinds
|
||||
|
||||
(provide define-type-alias
|
||||
★ ⇒ Int Bool String Float Char → ∀ tyλ tyapp
|
||||
(typed-out [+ : (→ Int Int Int)])
|
||||
λ #%app #%datum Λ inst ann)
|
||||
|
||||
(define-syntax-category kind)
|
||||
|
||||
;; redefine:
|
||||
;; - current-type?: well-formed types have kind ★
|
||||
;; - current-any-type?: valid types have any valid kind
|
||||
;; - current-type-eval: reduce tylams and tyapps
|
||||
;; - current-type=?: must compare kind annotations as well
|
||||
(begin-for-syntax
|
||||
|
||||
;; well-formed types have kind ★
|
||||
;; (need this for define-primop, which still uses type stx-class)
|
||||
(current-type? (λ (t) (★? (kindof t))))
|
||||
;; o.w., a valid type is one with any valid kind
|
||||
(current-any-type? (λ (t) ((current-kind?) (kindof t))))
|
||||
|
||||
;; TODO: I think this can be simplified
|
||||
(define (normalize τ)
|
||||
(syntax-parse τ #:literals (#%plain-app #%plain-lambda)
|
||||
[x:id #'x]
|
||||
[(#%plain-app
|
||||
(#%plain-lambda (tv ...) τ_body) τ_arg ...)
|
||||
(normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
|
||||
[(#%plain-lambda (x ...) . bodys)
|
||||
#:with bodys_norm (stx-map normalize #'bodys)
|
||||
(transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)]
|
||||
[(#%plain-app x:id . args)
|
||||
#:with args_norm (stx-map normalize #'args)
|
||||
(transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)]
|
||||
[(#%plain-app . args)
|
||||
#:with args_norm (stx-map normalize #'args)
|
||||
#:with res (normalize #'(#%plain-app . args_norm))
|
||||
(transfer-stx-props #'res τ #:ctx τ)]
|
||||
[_ τ]))
|
||||
(define old-eval (current-type-eval))
|
||||
(current-type-eval (lambda (τ) (normalize (old-eval τ))))
|
||||
(current-ev (current-type-eval))
|
||||
|
||||
(define old-type=? (current-type=?))
|
||||
; ty=? == syntax eq and syntax prop eq
|
||||
(define (type=? t1 t2)
|
||||
(let ([k1 (kindof t1)][k2 (kindof t2)])
|
||||
; the extra `and` and `or` clauses are bc type=? is a structural
|
||||
; traversal on stx objs, so not all sub stx objs will have a "type"-stx
|
||||
(and (or (and (not k1) (not k2))
|
||||
(and k1 k2 ((current-kind=?) k1 k2)))
|
||||
(old-type=? t1 t2))))
|
||||
(current-type=? type=?)
|
||||
(current-typecheck-relation type=?)
|
||||
(current=? type=?)
|
||||
(current-check-relation type=?))
|
||||
|
||||
;; kinds ----------------------------------------------------------------------
|
||||
(define-internal-kind-constructor ★) ; defines ★-
|
||||
(define-syntax (★ stx)
|
||||
(syntax-parse stx
|
||||
[:id (mk-kind #'(★-))]
|
||||
[(_ k:kind ...) (mk-kind #'(★- k.norm ...))]))
|
||||
|
||||
(define-kind-constructor ⇒ #:arity >= 1)
|
||||
|
||||
;; types ----------------------------------------------------------------------
|
||||
(define-kinded-syntax (define-type-alias alias:id τ:any-type) ≫
|
||||
------------------
|
||||
[≻ (define-syntax- alias
|
||||
(make-variable-like-transformer #'τ.norm))])
|
||||
|
||||
(define-base-type Int : ★)
|
||||
(define-base-type Bool : ★)
|
||||
(define-base-type String : ★)
|
||||
(define-base-type Float : ★)
|
||||
(define-base-type Char : ★)
|
||||
|
||||
(define-internal-type-constructor →) ; defines →-
|
||||
(define-kinded-syntax (→ ty ...+) ≫
|
||||
[⊢ ty ≫ ty- ⇒ (~★ . _)] ...
|
||||
--------
|
||||
[⊢ (→- ty- ...) ⇒ ★])
|
||||
|
||||
(define-internal-binding-type ∀) ; defines ∀-
|
||||
(define-kinded-syntax ∀ #:datum-literals (:)
|
||||
[(_ ([tv:id : k_in:kind] ...) ty) ≫
|
||||
[[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
|
||||
-------
|
||||
[⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]])
|
||||
|
||||
(define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
|
||||
[[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
|
||||
#:fail-unless ((current-kind?) #'k_body)
|
||||
(format "not a valid type: ~a\n" (type->str #'τ_body))
|
||||
--------
|
||||
[⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
|
||||
|
||||
(define-kinded-syntax (tyapp τ_fn τ_arg ...) ≫
|
||||
[⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
|
||||
#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
|
||||
(num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
|
||||
[⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
|
||||
--------
|
||||
[⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out])
|
||||
|
||||
;; terms ----------------------------------------------------------------------
|
||||
(define-typed-syntax λ #:datum-literals (:)
|
||||
[(_ ([x:id : τ_in:type] ...) e) ≫
|
||||
[[x ≫ x- : τ_in.norm] ... ⊢ e ≫ e- ⇒ τ_out]
|
||||
-------
|
||||
[⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]
|
||||
[(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
|
||||
[[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out]
|
||||
---------
|
||||
[⊢ (λ- (x- ...) e-)]])
|
||||
|
||||
(define-typed-syntax (#%app e_fn e_arg ...) ≫
|
||||
[⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]
|
||||
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
||||
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
|
||||
[⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
|
||||
--------
|
||||
[⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])
|
||||
|
||||
(define-typed-syntax (ann e (~datum :) τ:type) ≫
|
||||
[⊢ e ≫ e- ⇐ τ.norm]
|
||||
--------
|
||||
[⊢ e- ⇒ τ.norm])
|
||||
|
||||
(define-typed-syntax #%datum
|
||||
[(_ . b:boolean) ≫
|
||||
--------
|
||||
[⊢ (#%datum- . b) ⇒ Bool]]
|
||||
[(_ . s:str) ≫
|
||||
--------
|
||||
[⊢ (#%datum- . s) ⇒ String]]
|
||||
[(_ . f) ≫
|
||||
#:when (flonum? (syntax-e #'f))
|
||||
--------
|
||||
[⊢ (#%datum- . f) ⇒ Float]]
|
||||
[(_ . c:char) ≫
|
||||
--------
|
||||
[⊢ (#%datum- . c) ⇒ Char]]
|
||||
[(_ . n:integer) ≫
|
||||
--------
|
||||
[⊢ (#%datum- . n) ⇒ Int]]
|
||||
[(_ . x) ≫
|
||||
--------
|
||||
[_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
|
||||
|
||||
(define-typed-syntax (Λ bvs:kind-ctx e) ≫
|
||||
[([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
|
||||
--------
|
||||
[⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
|
||||
|
||||
;; TODO: what to do when a def-typed-stx needs both
|
||||
;; current-typecheck-relation and current-kindcheck-relation
|
||||
(define-typed-syntax (inst e τ ...) ≫
|
||||
[⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))]
|
||||
; [⊢ τ ≫ τ- ⇐ k] ...
|
||||
;; want to use kindchecks? instead of typechecks?
|
||||
[⊢ τ ≫ τ- ⇒ k_τ] ...
|
||||
#:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
|
||||
(typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
|
||||
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
|
||||
--------
|
||||
[⊢ e- ⇒ τ-inst])
|
||||
|
||||
|
|
@ -7,12 +7,14 @@
|
|||
|
||||
;; example suggested by Alexis King
|
||||
|
||||
;; this version still uses ':: key for kinds
|
||||
|
||||
(provide define-type-alias
|
||||
★ ⇒ Int Bool String Float Char → ∀ tyλ tyapp
|
||||
(typed-out [+ : (→ Int Int Int)])
|
||||
λ #%app #%datum Λ inst ann)
|
||||
|
||||
(define-syntax-category kind)
|
||||
(define-syntax-category :: kind)
|
||||
|
||||
;; redefine:
|
||||
;; - current-type?: well-formed types have kind ★
|
||||
|
|
@ -78,11 +80,11 @@
|
|||
[≻ (define-syntax- alias
|
||||
(make-variable-like-transformer #'τ.norm))])
|
||||
|
||||
(define-base-type Int : ★)
|
||||
(define-base-type Bool : ★)
|
||||
(define-base-type String : ★)
|
||||
(define-base-type Float : ★)
|
||||
(define-base-type Char : ★)
|
||||
(define-base-type Int :: ★)
|
||||
(define-base-type Bool :: ★)
|
||||
(define-base-type String :: ★)
|
||||
(define-base-type Float :: ★)
|
||||
(define-base-type Char :: ★)
|
||||
|
||||
(define-internal-type-constructor →) ; defines →-
|
||||
(define-kinded-syntax (→ ty ...+) ≫
|
||||
|
|
@ -91,15 +93,15 @@
|
|||
[⊢ (→- ty- ...) ⇒ ★])
|
||||
|
||||
(define-internal-binding-type ∀) ; defines ∀-
|
||||
(define-kinded-syntax ∀ #:datum-literals (:)
|
||||
[(_ ([tv:id : k_in:kind] ...) ty) ≫
|
||||
[[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
|
||||
(define-kinded-syntax ∀
|
||||
[(_ ctx:kind-ctx ty) ≫
|
||||
[[ctx.x ≫ tv- :: ctx.kind] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
|
||||
-------
|
||||
[⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]])
|
||||
[⊢ (∀- (tv- ...) ty-) ⇒ (★ ctx.kind ...)]])
|
||||
|
||||
(define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
|
||||
[[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
|
||||
#:fail-unless ((current-kind?) #'k_body)
|
||||
[[bvs.x ≫ tv- :: bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
|
||||
#:fail-unless ((current-kind?) #'k_body) ; better err, in terms of τ_body
|
||||
(format "not a valid type: ~a\n" (type->str #'τ_body))
|
||||
--------
|
||||
[⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
|
||||
|
|
@ -158,19 +160,21 @@
|
|||
[_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
|
||||
|
||||
(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)])
|
||||
|
||||
;; TODO: what to do when a def-typed-stx needs both
|
||||
;; current-typecheck-relation and current-kindcheck-relation
|
||||
(define-typed-syntax (inst e τ ...) ≫
|
||||
[⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))]
|
||||
; [⊢ τ ≫ τ- ⇐ k] ...
|
||||
;; want to use kindchecks? instead of typechecks?
|
||||
[⊢ τ ≫ τ- ⇒ k_τ] ...
|
||||
#:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
|
||||
(typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
|
||||
[⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~★ k ...))]
|
||||
;; switch to kindcheck? instead of typecheck?
|
||||
#:do[(define old-check (current-check-relation))
|
||||
(current-check-relation (current-kindcheck-relation))]
|
||||
[⊢ τ ≫ τ- ⇐ :: k] ...
|
||||
#:do[(current-check-relation old-check)]
|
||||
;; #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
|
||||
;; (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
|
||||
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
|
||||
--------
|
||||
[⊢ e- ⇒ τ-inst])
|
||||
|
|
|
|||
|
|
@ -1,57 +1,33 @@
|
|||
#lang turnstile/lang
|
||||
(extends "sysf.rkt" #:except #%datum ∀ ∀- ~∀ ∀? Λ inst)
|
||||
(reuse String #%datum #:from "stlc+reco+var.rkt")
|
||||
(reuse λ #%app Int → + #:from "sysf.rkt")
|
||||
(reuse define-type-alias #%datum String #:from "ext-stlc.rkt")
|
||||
|
||||
;; System F_omega
|
||||
;; Type relation:
|
||||
;; Types:
|
||||
;; - types from sysf.rkt
|
||||
;; - String from stlc+reco+var
|
||||
;; - redefine ∀
|
||||
;; - extend sysf with tyλ and tyapp
|
||||
;; Terms:
|
||||
;; - extend ∀ Λ inst from sysf
|
||||
;; - add tyλ and tyapp
|
||||
;; - #%datum from stlc+reco+var
|
||||
;; - extend sysf with Λ inst
|
||||
|
||||
(provide (for-syntax current-kind?)
|
||||
define-type-alias
|
||||
(type-out ★ ⇒ ∀★ ∀)
|
||||
Λ inst tyλ tyapp)
|
||||
(provide (type-out ∀) (kind-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)
|
||||
; are treated as kinds
|
||||
; <= define ★ as rename-transformer expanding to #%type
|
||||
;; want #%type to be equiv to ★
|
||||
;; => extend current-kind? to recognize #%type
|
||||
;; <= define ★ as rename-transformer expanding to #%type
|
||||
(begin-for-syntax
|
||||
(current-kind? (λ (k) (or (#%type? k) (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) (define k (kindof t))
|
||||
#;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
|
||||
(and k ((current-kind?) k) (not (⇒? k)))))
|
||||
;; o.w., a valid type is one with any valid kind
|
||||
;; any valid type (includes ⇒-kinded types)
|
||||
(current-any-type? (λ (t) (define k (kindof t))
|
||||
(and k ((current-kind?) k)))))
|
||||
|
||||
|
||||
; must override, to handle kinds
|
||||
(define-syntax define-type-alias
|
||||
(syntax-parser
|
||||
[(define-type-alias alias:id τ)
|
||||
#:with (τ- k_τ) (infer+erase #'τ #:tag '::)
|
||||
#:fail-unless ((current-kind?) #'k_τ)
|
||||
(format "not a valid type: ~a\n" (type->str #'τ))
|
||||
#'(define-syntax alias
|
||||
(syntax-parser [x:id #'τ-] [(_ . rst) #'(τ- . rst)]))]))
|
||||
(and k ((current-kind?) k))))
|
||||
;; well-formed types, ie not types with ⇒ kind
|
||||
(current-type? (λ (t) (and ((current-any-type?) t)
|
||||
(not (⇒? (kindof t)))))))
|
||||
|
||||
(begin-for-syntax
|
||||
(define ★? #%type?)
|
||||
(define-syntax ~★ (lambda _ (error "~★ not implemented")))) ; placeholder
|
||||
(define-syntax ~★ (λ _ (error "~★ not implemented")))) ; placeholder
|
||||
(define-syntax ★ (make-rename-transformer #'#%type))
|
||||
(define-kind-constructor ⇒ #:arity >= 1)
|
||||
(define-kind-constructor ∀★ #:arity >= 0)
|
||||
|
|
@ -59,7 +35,7 @@
|
|||
(define-binding-type ∀ #:arr ∀★)
|
||||
|
||||
;; alternative: normalize before type=?
|
||||
; but then also need to normalize in current-promote
|
||||
;; but then also need to normalize in current-promote
|
||||
(begin-for-syntax
|
||||
(define (normalize τ)
|
||||
(syntax-parse τ #:literals (#%plain-app #%plain-lambda)
|
||||
|
|
@ -80,38 +56,38 @@
|
|||
[_ τ]))
|
||||
|
||||
(define old-eval (current-type-eval))
|
||||
(define (type-eval τ) (normalize (old-eval τ)))
|
||||
(current-type-eval type-eval)
|
||||
(current-ev type-eval)
|
||||
(define (new-type-eval τ) (normalize (old-eval τ)))
|
||||
(current-type-eval new-type-eval)
|
||||
(current-ev new-type-eval)
|
||||
|
||||
(define old-type=? (current-type=?))
|
||||
; ty=? == syntax eq and syntax prop eq
|
||||
(define (type=? t1 t2)
|
||||
;; need to also compare kinds of types
|
||||
(define (new-type=? t1 t2)
|
||||
(let ([k1 (kindof t1)][k2 (kindof t2)])
|
||||
;; need these `not` checks bc type= does a structural stx traversal
|
||||
;; and may compare non-type ids (like #%plain-app)
|
||||
(and (or (and (not k1) (not k2))
|
||||
(and k1 k2 ((current-kind=?) k1 k2)))
|
||||
(old-type=? t1 t2))))
|
||||
(current-type=? type=?)
|
||||
(current-typecheck-relation type=?)
|
||||
(current-check-relation type=?))
|
||||
(current-type=? new-type=?)
|
||||
(current-typecheck-relation new-type=?)
|
||||
(current-check-relation new-type=?))
|
||||
|
||||
(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)])
|
||||
|
||||
(define-typed-syntax (inst e τ:any-type ...) ≫
|
||||
[⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~∀★ k ...))]
|
||||
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body) (⇒ :: (~∀★ k ...))]
|
||||
[⊢ τ ≫ τ- ⇐ :: k] ...
|
||||
#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
|
||||
--------
|
||||
[⊢ e- ⇒ τ-inst])
|
||||
[⊢ e- ⇒ #,(substs #'(τ- ...) #'tvs #'τ_body)])
|
||||
|
||||
;; TODO: merge with regular λ and app?
|
||||
;; - see fomega2.rkt
|
||||
;; - see fomega2.rkt for example with no explicit tyλ and tyapp
|
||||
(define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
|
||||
[[bvs.x ≫ tv- :: bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
|
||||
#:fail-unless ((current-kind?) #'k_body)
|
||||
#:fail-unless ((current-kind?) #'k_body) ; better err, in terms of τ_body
|
||||
(format "not a valid type: ~a\n" (type->str #'τ_body))
|
||||
--------
|
||||
[⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
|
||||
|
|
@ -119,7 +95,7 @@
|
|||
(define-kinded-syntax (tyapp τ_fn τ_arg ...) ≫
|
||||
[⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
|
||||
#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
|
||||
(num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
|
||||
(num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
|
||||
[⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
|
||||
--------
|
||||
[⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out])
|
||||
|
|
|
|||
213
turnstile/examples/tests/fomega-no-reuse-tests-old.rkt
Normal file
213
turnstile/examples/tests/fomega-no-reuse-tests-old.rkt
Normal file
|
|
@ -0,0 +1,213 @@
|
|||
#lang s-exp "../fomega-no-reuse-old.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; similar to fomega-tests.rkt, but with ': kind key
|
||||
|
||||
(check-type Int : ★)
|
||||
(check-type String : ★)
|
||||
(typecheck-fail →)
|
||||
(check-type (→ Int Int) : ★)
|
||||
(typecheck-fail (→ →))
|
||||
(typecheck-fail (→ 1))
|
||||
(check-type 1 : Int)
|
||||
|
||||
(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1")
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
|
||||
(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
|
||||
(∀ ([X : (★ ★)]) (→ X X)))
|
||||
|
||||
;(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 (tyλ ([t : ★]) t) : (⇒ ★ ★))
|
||||
(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
|
||||
(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
|
||||
(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
|
||||
|
||||
(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
|
||||
(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
|
||||
(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
|
||||
|
||||
;; partial-apply →
|
||||
(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
|
||||
: (⇒ ★ ★))
|
||||
;; f's type must have kind ★
|
||||
(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
|
||||
(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
|
||||
(∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
|
||||
(check-type (inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
: (→ (→ Int String) (→ Int String)))
|
||||
(typecheck-fail
|
||||
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
|
||||
#:with-msg "inst: type mismatch.*expected:.*★.*given:.*Int.*expressions: 1")
|
||||
|
||||
(typecheck-fail
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
#:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
|
||||
;; applied f too early
|
||||
(typecheck-fail
|
||||
(inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
#:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
|
||||
(check-type ((inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) : (→ Int String))
|
||||
(check-type (((inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([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 (tyλ ([X : ★]) X))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
|
||||
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
|
||||
|
||||
;; tapl examples, p451
|
||||
(define-type-alias Pair (tyλ ([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 (tyapp 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 (tyapp 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")
|
||||
: (tyapp 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 : ★]) (→ (tyapp 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)
|
||||
: (→ (tyapp 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 : ★]) (→ (tyapp 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)
|
||||
: (→ (tyapp 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)
|
||||
|
|
@ -1,84 +1,84 @@
|
|||
#lang s-exp "../fomega-no-reuse.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; identical to fomega-tests.rkt
|
||||
;; mostly identical to fomega-tests.rkt
|
||||
|
||||
(check-type Int : ★)
|
||||
(check-type String : ★)
|
||||
(check-type Int :: ★)
|
||||
(check-type String :: ★)
|
||||
(typecheck-fail →)
|
||||
(check-type (→ Int Int) : ★)
|
||||
(check-type (→ Int Int) :: ★)
|
||||
(typecheck-fail (→ →))
|
||||
(typecheck-fail (→ 1))
|
||||
(check-type 1 : Int)
|
||||
|
||||
(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1")
|
||||
(typecheck-fail (tyλ ([x :: ★]) 1) #:with-msg "not a valid type: 1")
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
|
||||
(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
|
||||
(∀ ([X : (★ ★)]) (→ X X)))
|
||||
(check-type (Λ ([X :: ★]) (λ ([x : X]) x)) : (∀ ([X :: ★]) (→ X X)))
|
||||
(check-not-type (Λ ([X :: ★]) (λ ([x : X]) x)) :
|
||||
(∀ ([X :: (★ ★)]) (→ X X)))
|
||||
|
||||
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
|
||||
(check-type (∀ ([t : ★]) (→ t t)) : (★ ★))
|
||||
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int 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)))
|
||||
|
||||
(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 (tyλ ([t : ★]) t) : (⇒ ★ ★))
|
||||
(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
|
||||
(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
|
||||
(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
|
||||
(check-type (tyλ ([t :: ★]) t) :: (⇒ ★ ★))
|
||||
(check-type (tyλ ([t :: ★] [s :: ★]) t) :: (⇒ ★ ★ ★))
|
||||
(check-type (tyλ ([t :: ★]) (tyλ ([s :: ★]) t)) :: (⇒ ★ (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t :: (⇒ ★ ★)]) t) :: (⇒ (⇒ ★ ★) (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t :: (⇒ ★ ★ ★)]) t) :: (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
|
||||
(check-type (tyλ ([arg :: ★] [res :: ★]) (→ arg res)) :: (⇒ ★ ★ ★))
|
||||
|
||||
(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
|
||||
(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
|
||||
(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
|
||||
(check-type (tyapp (tyλ ([t :: ★]) t) Int) :: ★)
|
||||
(check-type (λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) x) : (→ Int Int))
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) x) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
|
||||
(typecheck-fail ((λ ([x : (tyapp (tyλ ([t :: ★]) t) Int)]) (+ 1 x)) "a-string"))
|
||||
|
||||
;; partial-apply →
|
||||
(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
|
||||
: (⇒ ★ ★))
|
||||
(check-type (tyapp (tyλ ([arg :: ★]) (tyλ ([res :: ★]) (→ arg res))) Int)
|
||||
:: (⇒ ★ ★))
|
||||
;; f's type must have kind ★
|
||||
(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
|
||||
(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
|
||||
(∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
|
||||
(typecheck-fail (λ ([f : (tyapp (tyλ ([arg :: ★]) (tyλ ([res :: ★]) (→ arg res))) Int)]) f))
|
||||
(check-type (Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
|
||||
(∀ ([tyf :: (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
|
||||
(check-type (inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
(Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg :: ★]) (tyλ ([res :: ★]) (→ arg res))) Int))
|
||||
: (→ (→ Int String) (→ Int String)))
|
||||
(typecheck-fail
|
||||
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
|
||||
#:with-msg "inst: type mismatch.*expected:.*★.*given:.*Int.*expressions: 1")
|
||||
(typecheck-fail ; TODO: fix err msg: "given an invalid expression"
|
||||
(inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
|
||||
#:with-msg "inst: type mismatch: expected ★")
|
||||
|
||||
(typecheck-fail
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
(Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
#:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
|
||||
;; applied f too early
|
||||
(typecheck-fail
|
||||
(inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
(Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
(tyapp (tyλ ([arg :: ★]) (tyλ ([res :: ★]) (→ arg res))) Int))
|
||||
#:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
|
||||
(check-type ((inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
(Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg :: ★]) (tyλ ([res :: ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) : (→ Int String))
|
||||
(check-type (((inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
(Λ ([tyf :: (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg :: ★]) (tyλ ([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 (tyλ ([X : ★]) X))
|
||||
(define-type-alias Id (tyλ ([X :: ★]) X))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
|
||||
|
|
@ -91,104 +91,104 @@
|
|||
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
|
||||
|
||||
;; tapl examples, p451
|
||||
(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
|
||||
(define-type-alias Pair (tyλ ([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 (tyapp Pair X Y))))
|
||||
(Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
|
||||
: (∀ ([X :: ★][Y :: ★]) (→ X Y (tyapp 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 (tyapp 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")
|
||||
: (tyapp 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 : ★]) (→ (tyapp Pair X Y) X)))
|
||||
(Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
|
||||
: (∀ ([X :: ★][Y :: ★]) (→ (tyapp 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)
|
||||
: (→ (tyapp 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 : ★]) (→ (tyapp Pair X Y) Y)))
|
||||
(Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
|
||||
: (∀ ([X :: ★][Y :: ★]) (→ (tyapp 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)
|
||||
: (→ (tyapp 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)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,8 @@
|
|||
#lang s-exp "../fomega.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; ok to conflate check-kind and check-type bc
|
||||
;; kindcheck? does not require special cases
|
||||
(check-type Int :: ★)
|
||||
(check-type String :: ★)
|
||||
(typecheck-fail →)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user