first take on match-define-like form

racket/typed/core-expressions.rkt

@@ -9,10 +9,14 @@
          let
          let*
          cond
+         else
          match
          tuple
+         unit
          select
          error
+         define-tuple
+         match-define
          (for-syntax (all-defined-out)))
 
 (require "core-types.rkt")
@@ -74,11 +78,11 @@
 
 (define-typed-syntax (when e s ...+) ≫
   ------------------------------------
-  [≻ (if e (begin s ...) #f)])
+  [≻ (if e (let () s ...) #f)])
 
 (define-typed-syntax (unless e s ...+) ≫
   ------------------------------------
-  [≻ (if e #f (begin s ...))])
+  [≻ (if e #f (let () s ...))])
 
 ;; copied from ext-stlc
 (define-typed-syntax let
@@ -129,6 +133,8 @@
      (⇒ ν-f #,(make-Branch #'((fs ...) ...)))
      (⇒ ν-s (ss ... ...))])
 
+(define else #t)
+
 (define-typed-syntax (match e [p s ...+] ...+) ≫
   [⊢ e ≫ e- (⇒ : τ-e)]
   #:fail-unless (pure? #'e-) "expression must be pure"
@@ -160,6 +166,8 @@
   -----------------------
   [⊢ (#%app- list- 'tuple e- ...) (⇒ : (Tuple τ ...))])
 
+(define unit : Unit (tuple))
+
 (define-typed-syntax (select n:nat e:expr) ≫
   [⊢ e ≫ e- (⇒ : (~Tuple τ ...))]
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"
@@ -227,3 +235,42 @@
                    #'list
                    identity
                    (lambda (exp) #`(==- #,exp))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Derived Forms
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-typed-syntax (define-tuple (x:id ...) e:expr) ≫
+  [⊢ e ≫ e- (⇒ (~Tuple τ ...))]
+  #:fail-unless (stx-length=? #'(x ...) #'(τ ...))
+                "mismatched size"
+  #:fail-unless (pure? #'e-) "expr must be pure"
+  #:with (sel ...) (for/list ([y (in-syntax #'(x ...))]
+                              [t (in-syntax #'(τ ...))]
+                              [i (in-naturals)])
+                     (quasisyntax/loc this-syntax
+                       (select #,i it)))
+  ----------------------------------------
+  [≻ (begin
+       (define it e-)
+       (define x : τ sel) ...)])
+
+(define-typed-syntax (match-define pat:expr e:expr) ≫
+  #:with ([x τ] ...) (pat-bindings #'pat)
+  ----------------------------------------
+  [≻ (define-tuple (x ...)
+       (match e
+         [pat
+          (tuple x ...)]))])
+
+;; extremely limited match-define for `define-constructor`-d things
+
+#;(define-typed-syntax (match-define (~constructor-exp ctor x:id ...) e:expr) ≫
+  [⊢ e ≫ e- (⇒ (~constructor-type tag1 τ ...))]
+  #:fail-unless (stx-length=? #'(x ...) #'(τ ...))
+                "mismatched size"
+  [⊢ (ctor (bind x τ) ...) ≫ pat- (⇒ (~constructor-type tag2 _ ...))]
+  #:fail-unless (equal? #'tag1 #'tag2)
+                (~format "type mismatch: ~a, ~a" #'tag1 #'tag2)
+  ------------------------------------------------------------
+  )

racket/typed/core-types.rkt

@@ -249,6 +249,7 @@
             #'τ.norm]))]))
 
 (define-type-alias ⊥ (U*))
+(define-type-alias Unit (Tuple))
 
 (define-for-syntax (prune+sort tys)
   (stx-sort
@@ -1203,7 +1204,7 @@
    #:do [(define-values (e-... τ... ep-effs f-effs s-effs) (walk/bind #'(e_unit ... e)))]
    #:with τ (last τ...)
    --------
-   [⊢ (let- () #,@e-...) (⇒ : τ)
+   [⊢ (begin- #,@e-...) (⇒ : τ)
       (⇒ ν-ep (#,@ep-effs))
       (⇒ ν-f (#,@f-effs))
       (⇒ ν-s (#,@s-effs))]])