Added pre-definition type ascription

README.md

@@ -45,6 +45,10 @@ Try it out: open up DrRacket and put the following in the definition area:
 (if true
     false
     true)
+
+(: + (-> Nat Nat Nat))
+(define + plus)
+(+ z (s z))
 ```
 
 Try entering the following in the interaction area:

cur-doc/cur/scribblings/stdlib/sugar.scrbl

@@ -62,10 +62,24 @@ Defines multi-arity procedure application via automatic currying.
           (conj Bool Bool true false)]
 }
 
+@defform[(: name type)]{
+Declare that the @emph{function} which will be defined as @racket[name] has type @racket[type].
+Must precede the definition of @racket[name].
+@racket[type] must expand to a function type of the form @racket[(Π (x : t1) t2)]
+When used, this form allows omitting the annotations on arguments in the definition @racket[name]
+}
+
 @defform*[((define name body)
-           (define (name (x : t) ...) body))]{
+           (define (name x ...) body)
+	   (define (name (x : t) ...) body))]{
 Like the @racket[define] provided by @racketmodname[cur], but supports
 defining curried functions via @racket[lambda].
+The second form, @racket[(define (name x ...) body)], can only be used when
+a @racket[(: name type)] form appears earlier in the module.
+
+@examples[#:eval curnel-eval
+          (: id (forall (A : Type) (a : A) A))
+	  (define (id A a) a)]
 }
 
 @defform[(elim type motive-result-type e ...)]{

cur-lib/cur/stdlib/sugar.rkt

@@ -11,6 +11,7 @@
     [lambda λ])
   #%app
   define
+  :
   elim
   define-type
   match
@@ -104,9 +105,57 @@
     [(_ name type)
      (define name type)]))
 
+;; Cooperates with define to allow Haskell-esque type annotations
+#| TODO NB:
+ | This method of cooperating macros is sort of a terrible
+ | hack. Instead, need principled way of adding/retrieving information
+ | to/from current module. E.g. perhaps provide extensions an interface to
+ | module's term environment and inductive signature. Then, :: could add
+ | new "id : type" to environment, and define could extract type and use.
+ |#
+(begin-for-syntax
+  (define annotation-dict (make-hash))
+  (define (annotation->types type-syn)
+    (let loop ([ls '()]
+               [syn type-syn])
+      (syntax-parse (cur-expand syn)
+        #:datum-literals (:)
+        [(real-Π (x:id : type) body)
+         (loop (cons #'type ls) #'body)]
+        [_ (reverse ls)]))))
+
+(define-syntax (: syn)
+  (syntax-parse syn
+    [(_ name:id type:expr)
+     ;; NB: Unhygenic; need to reuse Racket's identifiers, and make this type annotation a syntax property
+     (syntax-parse (cur-expand #'type)
+      #:datum-literals (:)
+      [(real-Π (x:id : type) body) (void)]
+      [_
+       (raise-syntax-error
+        ':
+        "Can only declare annotations for functions, but not a function type"
+        syn)])
+     (dict-set! annotation-dict (syntax->datum #'name) (annotation->types #'type))
+     #'(void)]))
+
 ;; TODO: Allow inferring types as in above TODOs for lambda, forall
 (define-syntax (define syn)
-  (syntax-case syn ()
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(define (name:id x:id ...) body)
+     (cond
+       [(dict-ref annotation-dict (syntax->datum #'name)) =>
+        (lambda (anns)
+          (quasisyntax/loc syn
+            (real-define name (lambda #,@(for/list ([x (syntax->list #'(x ...))]
+                                                    [type anns])
+                                           #`(#,x : #,type)) body))))]
+       [else
+        (raise-syntax-error
+         'define
+         "Cannot omit type annotations unless you have declared them with (: name type) form first."
+         syn)])]
     [(define (name (x : t) ...) body)
      (quasisyntax/loc syn
        (real-define name (lambda (x : t) ... body)))]
@@ -355,8 +404,8 @@
     [(let (c:let-clause ...) body)
      #'((lambda (c.id : c.type) ... body) c.e ...)]))
 
-;; Normally type checking will only happen if a term is actually used. This forces a term to be
+;; Normally type checking will only happen if a term is actually used/appears at top-level.
-;; checked against a particular type.
+;; This forces a term to be checked against a particular type.
 (define-syntax (:: syn)
   (syntax-case syn ()
     [(_ pf t)

cur-test/cur/tests/plus.rkt

@@ -0,0 +1,24 @@
+#lang cur
+
+(require
+ cur/stdlib/sugar
+ rackunit)
+
+(data Nat : Type
+  (z : Nat)
+  (s : (Π (x : Nat) Nat)))
+
+(plus . : . (-> Nat Nat Nat))
+(define (plus n m)
+  (match n
+    [z m]
+    [(s (x : Nat))
+     (s (recur x))]))
+
+(check-equal?
+ (plus z z)
+ z)
+
+(check-equal?
+ (plus (s z) z)
+ (s z))