Add : declarations for val definitions

hackett-lib/hackett/private/base.rkt

@@ -6,7 +6,9 @@
                      syntax/parse/experimental/template
                      syntax/intdef
                      syntax/srcloc
-                     threading)
+                     syntax/parse/class/local-value
+                     threading
+                     serialize-syntax-introducer)
          (postfix-in - (combine-in racket/base
                                    racket/promise))
          racket/stxparam
@@ -324,6 +326,37 @@
 
 ;; ---------------------------------------------------------------------------------------------------
 
+(begin-for-syntax
+  ; Instances of this struct are created by `:` when declaring the types of bindings
+  ; seperately from their definitions. When a binding is defined (with `def` or related
+  ; forms), it searches for a `binding-declaration` and fills in `internal-id` with the
+  ; actual definition. The `type` field is used as the expected type of the definition.
+  ; fixity : [Maybe Fixity]
+  (struct binding-declaration [internal-id type scoped-binding-introducer fixity]
+    #:property prop:procedure
+    (λ (this stx)
+      (match-define (binding-declaration x- type _ _) this)
+      ((make-typed-var-transformer x- type) stx))
+    #:property prop:infix-operator
+    (λ (this) (binding-declaration-fixity this)))
+
+  (define-syntax-class id/binding-declaration
+    #:attributes [internal-id type scoped-binding-introducer fixity]
+    [pattern (~var x (local-value binding-declaration?))
+             #:do [(match-define (binding-declaration x-* type* sbi* fixity*)
+                     (attribute x.local-value))]
+             #:attr internal-id (syntax-local-introduce x-*)
+             #:with type        (syntax-local-introduce type*)
+             #:attr scoped-binding-introducer (deserialize-syntax-introducer sbi*)
+             #:attr fixity      fixity*]))
+
+(define-syntax-parser define/binding-declaration
+  [(_ x:id/binding-declaration rhs)
+   #:with x- #'x.internal-id
+   #'(define- x- rhs)])
+
+;; ---------------------------------------------------------------------------------------------------
+
 (define-syntax-parser @%module-begin
   [(_ form ...)
    (~> (local-expand (value-namespace-introduce
@@ -343,20 +376,54 @@
   [(_ . x)
    (raise-syntax-error #f "literal not supported" #'x)])
 
-(define-syntax-parser :
-  ; The #:exact option prevents : from performing context reduction. This is not normally important,
-  ; but it is required for forms that use : to ensure an expression has a particular shape in order to
-  ; interface with untyped (i.e. Racket) code, and therefore the resulting type is ignored. For
-  ; example, the def form wraps an expression in its expansion with :, but it binds the actual
-  ; identifier to a syntax transformer that attaches the type directly. Therefore, it needs to perform
-  ; context reduction itself prior to expanding to :, and it must use #:exact.
-  [(_ e {~type t:type} {~optional {~and #:exact exact?}})
-   #:with t_reduced (if (attribute exact?)
-                        #'t.expansion
-                        (type-reduce-context #'t.expansion))
-   (attach-type #`(let-values- ([() t.residual])
-                  #,(τ⇐! ((attribute t.scoped-binding-introducer) #'e) #'t_reduced))
-                #'t_reduced)])
+;; The `:` form behaves differently in an expression context vs. a
+;; module context by dispatching on (syntax-local-context).
+(define-syntax :
+  (λ (stx)
+    (match (syntax-local-context)
+      ; In an expression context, `:` annotates an expression with
+      ; an expected type.
+      ['expression
+       (syntax-parse stx
+         ; The #:exact option prevents : from performing context reduction. This is not normally important,
+         ; but it is required for forms that use : to ensure an expression has a particular shape in order to
+         ; interface with untyped (i.e. Racket) code, and therefore the resulting type is ignored. For
+         ; example, the def form wraps an expression in its expansion with :, but it binds the actual
+         ; identifier to a syntax transformer that attaches the type directly. Therefore, it needs to perform
+         ; context reduction itself prior to expanding to :, and it must use #:exact.
+         [(_ e {~type t:type} {~optional {~and #:exact exact?}})
+          #:with t_reduced (if (attribute exact?)
+                               #'t.expansion
+                               (type-reduce-context #'t.expansion))
+          (attach-type #`(let-values- ([() t.residual])
+                                      #,(τ⇐! ((attribute t.scoped-binding-introducer) #'e) #'t_reduced))
+                       #'t_reduced)])]
+
+      ; In other contexts, such as module-level bindings or
+      ; in the REPL, : is a type declaration for `x`, and
+      ; will be understood by `def`.
+      [_
+       (syntax-parse stx
+         [(_ x:id {~type t:type}
+             {~alt {~optional {~and #:exact exact?}}
+                   {~optional f:fixity-annotation}}
+             ...)
+          #:with x- (generate-temporary #'x)
+          #:with exct? (and (attribute exact?) #true)
+          #:with fixity (attribute f.fixity)
+          #:with t_reduced (if (attribute exact?)
+                               #'t.expansion
+                               (type-reduce-context #'t.expansion))
+          #:with sbi (serialize-syntax-introducer
+                      (attribute t.scoped-binding-introducer))
+          #`(begin-
+              (define-values- [] t.residual)
+              (define-syntax- x
+                (binding-declaration
+                 (quote-syntax x-)
+                 (quote-syntax t_reduced)
+                 (quote-syntax sbi)
+                 'fixity)))])])))
 
 (define-syntax-parser λ1
   [(_ x:id e:expr)
@@ -383,31 +450,42 @@
 
 (define-syntax-parser def
   #:literals [:]
-  [(_ id:id
-      {~or {~once {~seq {~and : {~var :/use}} {~type t:type}
-                        {~optional {~and #:exact exact?}}}}
-           {~optional fixity:fixity-annotation}}
-      ...
+  [(_ x:id/binding-declaration e:expr)
+   #:with x- #'x.internal-id
+   (syntax-property
+    #`(define- x-
+        (: #,((attribute x.scoped-binding-introducer) #'e)
+           x.type
+           #:exact))
+    'disappeared-use
+    (syntax-local-introduce #'x))]
+
+  [(_ x:id {~and : {~var :/use}} type:expr
+      {~and {~seq stuff ...}
+            {~seq {~alt {~optional {~and #:exact exact?}}
+                        {~optional f:fixity-annotation}}
+                  ...}}
       e:expr)
-   #:with id- (generate-temporary #'id)
-   #:with t_reduced (if (attribute exact?) #'t.expansion (type-reduce-context #'t.expansion))
-   #`(begin-
-       #,(indirect-infix-definition
-          #'(define-syntax- id (make-typed-var-transformer #'id- (quote-syntax t_reduced)))
-          (attribute fixity.fixity))
-       (define- id- (:/use #,((attribute t.scoped-binding-introducer) #'e) t_reduced #:exact)))]
+   #'(begin-
+       (:/use x type stuff ...)
+       (def x e))]
+
   [(_ id:id
-      {~optional fixity:fixity-annotation}
+      {~and {~seq fixity-stuff ...}
+            {~optional fixity:fixity-annotation}}
       e:expr)
-   #:with x^ (generate-temporary)
+   #:with x^ (generate-temporary #'z)
    #:with t_e #'(#%type:wobbly-var x^)
    #:do [(match-define-values [(list id-) e-] (τ⇐/λ! #'e #'t_e (list (cons #'id #'t_e))))]
    #:with t_gen (type-reduce-context (generalize (apply-current-subst #'t_e)))
+   #:with id-/gen (attach-type id- #'t_gen)
    #`(begin-
-       #,(indirect-infix-definition
-          #`(define-syntax- id (make-typed-var-transformer (quote-syntax #,id-) (quote-syntax t_gen)))
-          (attribute fixity.fixity))
-       (define- #,id- #,e-))])
+       (: id t_gen fixity-stuff ... #:exact)
+       (define/binding-declaration id
+         (let-syntax ([id-/gen
+                       (make-rename-transformer (quote-syntax id))])
+           #,e-)))])
+
 
 (begin-for-syntax
   (struct todo-item (full summary) #:prefab))

hackett-lib/info.rkt

@@ -7,6 +7,7 @@
     "curly-fn-lib"
     "data-lib"
     "syntax-classes-lib"
-    "threading-lib"))
+    "threading-lib"
+    "serialize-syntax-introducer"))
 (define build-deps
   '())

hackett-test/tests/hackett/integration/id-decl.rkt

@@ -0,0 +1,22 @@
+#lang hackett
+
+(require hackett/private/test)
+
+(: f {Integer -> Integer})
+(def f (λ [x] (id x)))
+
+(: fact {Integer -> Integer})
+(defn fact 
+  [[0] 1]
+  [[n] {n * (fact {n - 1})}])
+
+(: id (forall [a] {a -> a}))
+(defn id
+  [[x] (: x a)])
+
+(: rmt (forall [a b] (Monoid b) => (Either a b)))
+(def rmt (Right (: mempty b)))
+
+(test {rmt ==! (: (Right "") (Either Unit String))})
+(test {rmt ==! (: (Right Nil) (Either Bool (List Integer)))})
+