turnstile is a grammar language created in 2017. Turnstile aims to help Racket programmers create typed languages. It does so with extensions of Racketβs macro-definition forms that facilitate implementation of type rules alongside normal macro code. As a result, the macros implementing a new language directly type check the program during expansion, obviating the need to create and call out to a separate type checker. Thus, a complete typed language implementation remains a series of macro definitions that may be imported and exported in the standard way that Racket programmers are accustomed to.
| #3884on PLDB | 5Years Old |
#lang turnstile
(provide β Int Ξ» #%app #%datum + ann)
(define-base-type Int)
(define-type-constructor β #:arity > 0)
(define-primop + : (β Int Int Int))
; [APP]
(define-typed-syntax (#%app e_fn e_arg ...) β«
[β’ e_fn β« e_fn- β (~β Ο_in ... Ο_out)]
#:fail-unless (stx-length=? #'[Ο_in ...] #'[e_arg ...])
(format "arity mismatch, expected ~a args, given ~a"
(stx-length #'[Ο_in ...]) #'[e_arg ...])
[β’ e_arg β« e_arg- β Ο_in] ...
--------
[β’ (#%app- e_fn- e_arg- ...) β Ο_out])
; [LAM]
(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-)]])
; [ANN]
(define-typed-syntax (ann e (~datum :) Ο:type) β«
[β’ e β« e- β Ο.norm]
--------
[β’ e- β Ο.norm])
; [DATUM]
(define-typed-syntax #%datum
[(_ . n:integer) β«
--------
[β’ (#%datum- . n) β Int]]
[(_ . x) β«
--------
[#:error (type-error #:src #'x
#:msg "Unsupported literal: ~v" #'x)]])