PLDB
Languages Patterns Calendar About Lists Join

turnstile

turnstile

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

Example code from the web:

#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)]])

Article source

PLDB - Build the next great programming language. v5.0.0 - Email Β· Github