Basics

To extend a language, e.g. mlish:

#lang turnstile/lang
(extends turnstile/examples/mlish)
(define-typed-syntax (blah e₁ e₂) ≫
  [⊢ e₁ ≫ e₁- ⇒ τ₁]
  [⊢ e₂ ≫ e₂- ⇒ τ₂]
  ----------
  [⊢ (new-expression which can use e₁- e₂-)
     ⇒ (new-result-type which can use τ₁ τ₂)])

Save this file in a package (raco pkg new mypkg on the command-line and save as mypkg/myfile.rkt, then cd mypkg/; raco pkg install). Then write a file using that new, extended language:

#lang s-exp mypkg/myfile
(blah (list 1 2 3) #t) ;; Can also use the things defined by mlish.

To get the type of an expression at compile-time

(define-typed-syntax (get-type e) ≫
  [⊢ e ≫ e- ⇒ τ]
  #:with foobar (do-ssomething-with #'τ)
  -----
  [⊢ (void) ⇒ Unit])

To get the pretty representation of a type at compile-time: type→str. So, to define a :type operator which returns the inferred type of its argument as a string:

(define-typed-syntax (:type e) ≫
  [⊢ e ≫ e- ⇒ τ]
  #:with s (type->str #'τ)
  -----
  [⊢ (#%datum- . s) ⇒ String])