simple-kinds.rkt

#lang turnstile/lang

(provide (rename-out [app #%app])
         Integer String Maybe)

(require (postfix-in - racket/base))

(define-syntax-category kind)
(define-base-kind ★)

(begin-for-syntax
  (current-type? (λ (t) (kind? (typeof t)))))

(define-type-constructor →-
  #:arity = 2
  #:arg-variances (const (list covariant contravariant))
  #:no-attach-kind
  #:no-provide)

(define-typed-syntax →
  [(_ a:type b:type) ≫
   [⊢ a ≫ a- ⇐ ★]
   [⊢ b ≫ b- ⇐ ★]
   -------------------
   [⊢ (→- a- b-) ⇒ ★]])

(define-typed-syntax λ
  #:datum-literals [:]
  [(_ [x:id : t_in:type] expr) ≫
   [[x ≫ x- : t_in.norm] ⊢ expr ≫ expr- ⇒ t_out]
   -----------------------------------------------
   [⊢ (λ- (x-) expr-) ⇒ (→ t_in.norm t_out)]]
  [(_ x:id expr) ⇐ (~→- t_in t_out) ≫
   [[x ≫ x- : t_in] ⊢ expr ≫ expr- ⇐ t_out]
   ------------------------------------------
   [⊢ (λ- (x-) expr-)]])

(define-typed-syntax app
  [(_ fn arg) ≫
   [⊢ fn ≫ fn- ⇒ (~→- t_in t_out)]
   [⊢ arg ≫ arg- ⇐ t_in]
   --------------------------------
   [⊢ (#%app- fn- arg-) ⇒ t_out]]
  [(_ fn arg args ...+) ≫
   ---------------------------
   [≻ ((app fn arg) args ...)]])

;; ---------------------------------------------------------------------------------------------------

(define-simple-macro (define-base-type: τ {~datum :} k)
  #:with τ- (generate-temporary #'τ)
  (begin
    (define-base-type τ- #:no-attach-kind #:no-provide)
    (define-syntax τ (make-variable-like-transformer (⊢ τ- : k)))))

(define-kind-constructor →k
  #:arity = 2
  #:arg-variances (const (list covariant contravariant)))

(define-base-type: Integer : ★)
(define-base-type: String : ★)

(define-base-type: Maybe : (→k ★ ★))

(define-typed-syntax #%datum
  [(_ . n:integer) ≫
   ----------------------------
   [⊢ (#%datum- . n) ⇒ Integer]]
  [(_ . n:str) ≫
   ---------------------------
   [⊢ (#%datum- . n) ⇒ String]]
  [(_ . x) ≫
   ----------------------------------------------------------------------
   [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])