46 lines
1.7 KiB
Racket
46 lines
1.7 KiB
Racket
#lang racket/base
|
|
(require
|
|
(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
|
|
"typecheck.rkt")
|
|
(provide (rename-out [λ/tc λ] [app/tc #%app]))
|
|
(provide #%module-begin #%top-interaction #%top require)
|
|
|
|
;; Simply-Typed Lambda Calculus
|
|
;; - no base type so cannot write any terms
|
|
;; Types: →
|
|
;; Terms:
|
|
;; - var
|
|
;; - multi-arg lambda
|
|
;; - multi-arg app
|
|
|
|
(define-type-constructor →)
|
|
|
|
(define-syntax (λ/tc stx)
|
|
(syntax-parse stx
|
|
[(_ (b:typed-binding ...) e)
|
|
#:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
|
|
(⊢ #'(λ xs- e-) #'(b.τ ... → τ_res))]))
|
|
|
|
(define-syntax (app/tc stx)
|
|
(syntax-parse stx #:literals (→)
|
|
[(_ e_fn e_arg ...)
|
|
#:with (e_fn- τ_fn) (infer+erase #'e_fn)
|
|
#:fail-unless (→? #'τ_fn)
|
|
(format "Type error: Attempting to apply a non-function ~a with type ~a\n"
|
|
(syntax->datum #'e_fn) (syntax->datum #'τ_fn))
|
|
#:with (τ ... → τ_res) #'τ_fn
|
|
#:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
|
|
#:fail-unless (types=? #'(τ ...) #'(τ_arg ...))
|
|
(string-append
|
|
(format
|
|
"Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
|
|
(syntax->datum #'e_fn))
|
|
(string-join
|
|
(map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
|
|
", ")
|
|
"\nexpect arguments with type: "
|
|
(string-join
|
|
(map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
|
|
", "))
|
|
(⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
|