Type Predicates for Function Types in Typed/Racket

Question

I'm at the early stages of designing a framework and am fooling around with typed/racket. Suppose I have the following types:

   (define-type Calculate-with-one-number (-> Number Number))
   (define-type Calculate-with-two-numbers (-> Number Number Number))

And I want to have a function that dispatches on type:

(: dispatcher (-> (U Calculate-with-one-number Calculate-with-two-numbers) Number))

(define (dispatcher f args)
   (cond [(Calculate-with-one-number? f)
          (do-something args)]
         [(Calculate-with-two-numbers? f)
          (do-something-else args)]
         [else 42]))

How do I create the type-predicates Calculate-with-one-number? and Calculate-with-two-numbers? in Typed/Racket? For non-function predicates I can use define-predicate. But it's not clear how to implement predicates for function types.

Answer 1

Since I am self answering, I'm taking the liberty to clarify the gist of my question in light of the discussion of arity as a solution. The difference in arity was due to my not considering its implications when specifying the question.

The Problem

In #lang typed/racket as in many Lisps, functions, or more properly: procedures, are first class dataypes.

By default, #lang racket types procedures by arity and any additional specificity in argument types must be done by contract. In #lang typed/racket procedures are typed both by arity and by the types of their arguments and return values due to the language's "baked-in contracts".

Math as an example

The Typed Racket Guide provides an example using define-type to define a procedure type:

 (define-type NN (-> Number Number))

This allows specifying a procedure more succinctly:

 ;; Takes two numbers, returns a number
 (define-type 2NN (-> Number Number Number))

 (: trigFunction1 2NN)
 (define (trigFunction1 x s)
   (* s (cos x)))

 (: quadraticFunction1 2NN)
 (define (quadraticFunction1 x b)
   (let ((x1 x))
     (+ b (* x1 x1))))

The Goal

In a domain like mathematics, it would be nice to work with more abstract procedure types because knowing that a function is cyclical between upper and lower bounds (like cos) versus having only one bound (e.g. our quadratic function) versus asymptotic (e.g. a hyperbolic function) provides for clearer reasoning about the problem domain. It would be nice to have access to abstractions something like:

 (define-type Cyclic2NN (-> Number Number Number))
 (define-type SingleBound2NN (-> Number Number Number))

 (: trigFunction1 Cyclic2NN)
 (define (trigFunction1 x s)
   (* s (cos x)))

 (: quadraticFunction1 SingleBound2NN)
 (define (quadraticFunction1 x b)
   (let ((x1 x))
     (+ b (* x1 x1))))

 (: playTone (-> Cyclic2NN))
 (define (playTone waveform)
   ...)

 (: rabbitsOnFarmGraph (-> SingleBound2NN)
 (define (rabbitsOnFarmGraph populationSize)
   ...)

Alas, define-type does not deliver this level of granularity when it comes to procedures. Even moreover, the brief false hope that we might easily wring such type differentiation for procedures manually using define-predicate is dashed by:

Evaluates to a predicate for the type t, with the type (Any -> Boolean : t). t may not contain function types, or types that may refer to mutable data such as (Vectorof Integer).

Fundamentally, types have uses beyond static checking and contracts. As first class members of the language, we want to be able to dispatch our finer grained procedure types. Conceptually, what is needed are predicates along the lines of Cyclic2NN? and SingleBound2NN?. Having only arity for dispatch using case-lambda just isn't enough.

Guidance from Untyped Racket

Fortunately, Lisps are domain specific languages for writing Lisps once we peal back the curtain to reveal the wizard, and in the end we can get what we want. The key is to come at the issue the other way and ask "How canwe use the predicates typed/racket gives us for procedures?"

Structures are Racket's user defined data types and are the basis for extending it's type system. Structures are so powerful that even in the class based object system, "classes and objects are implemented in terms of structure types."

In #lang racket structures can be applied as procedures giving the #:property keyword using prop:procedure followed by a procedure for it's value. The documentation provides two examples:

The first example specifies a field of the structure to be applied as a procedure. Obviously, at least once it has been pointed out, that field must hold a value that evaluates to a procedure.

> ;; #lang racket
> (struct annotated-proc (base note)
     #:property prop:procedure
      (struct-field-index base))
> (define plus1 (annotated-proc
     (lambda (x) (+ x 1))
     "adds 1 to its argument"))
> (procedure? plus1)
#t
> (annotated-proc? plus1)
#t
> (plus1 10)
11
> (annotated-proc-note plus1)
"adds 1 to its argument"

In the second example an anonymous procedure [lambda] is provided directly as part of the property value. The lambda takes an operand in the first position which is resolved to the value of the structure being used as a procedure. This allows accessing any value stored in any field of the structure including those which evaluate to procedures.

> ;; #lang racket
> (struct greeter (name)
    #:property prop:procedure
    (lambda (self other)
       (string-append
         "Hi " other
          ", I'm " (greeter-name self))))
> (define joe-greet (greeter "Joe"))
> (greeter-name joe-greet)
"Joe"
> (joe-greet "Mary")
"Hi Mary, I'm Joe"
> (joe-greet "John")
"Hi John, I'm Joe

Applying it to typed/racket

Alas, neither syntax works with struct as implemented in typed/racket. The problem it seems is that the static type checker as currently implemented cannot both define the structure and resolve its signature as a procedure at the same time. The right information does not appear to be available at the right phase when using typed/racket's struct special form.

To get around this, typed/racket provides define-struct/exec which roughly corresponds to the second syntactic form from #lang racket less the keyword argument and property definition:

    (define-struct/exec name-spec ([f : t] ...) [e : proc-t])

      name-spec     =       name
                    |       (name parent)

Like define-struct, but defines a procedural structure. The procdure e is used as the value for prop:procedure, and must have type proc-t.

Not only does it give us strongly typed procedural forms, it's a bit more elegant than the keyword syntax found in #lang racket. Example code to resolve the question as restated here in this answer is:

#lang typed/racket

(define-type 2NN (-> Number Number Number))

(define-struct/exec Cyclic2NN
   ((f : 2NN))
   ((lambda(self x s)
     ((Cyclic2NN-f self) x s))
      : (-> Cyclic2NN Number Number Number)))

 (define-struct/exec SingleBound2NN
   ((f : 2NN))
   ((lambda(self x s)
     ((SingleBound2NN-f self) x s))
       : (-> SingleBound2NN Number Number Number)))

 (define trigFunction1 
   (Cyclic2NN 
    (lambda(x s) 
      (* s (cos x)))))

(define quadraticFunction1
  (SingleBound2NN
    (lambda (x b)
      (let ((x1 x))
        (+ b (* x1 x1)))))

The defined procedures are strongly typed in the sense that:

> (SingleBound2NN? trigFunction1)
- : Boolean
#f
>  (SingleBound2NN? quadraticFunction1)
- : Boolean
#t

All that remains is writing a macro to simplify specification.

Answer 2

In the general case, what you want is impossible due to how types are implemented in Racket. Racket has contracts, which are run-time wrappers that guard parts of a program from other parts. A function contract is a wrapper that treats the function as a black box - a contract of the form (-> number? number?) can wrap any function and the new wrapper function first checks that it receives one number? and then passes it to the wrapped function, then checks that the wrapped function returns a number?. This is all done dynamically, every single time the function is called. Typed Racket adds a notion of types that are statically checked, but since it can provide and require values to and from untyped modules, those values are guarded with contracts that represent their type.

In your function dispatcher, you accept a function f dynamically, at run time and then want to do something based on what kind of function you got. But functions are black boxes - contracts don't actually know anything about the functions they wrap, they just check that they behave properly. There's no way to tell if dispatcher was given a function of the form (-> number? number?) or a function of the form (-> string? string?). Since dispatcher can accept any possible function, the functions are black boxes with no information about what they accept or promise. dispatcher can only assume the function is correct with a contract and try to use it. This is also why define-type doesn't make a predicate automatically for function types - there's no way to prove a function has the type dynamically, you can only wrap it in a contract and assume it behaves.

The exception to this is arity information - all functions know how many arguments they accept. The procedure-arity function will give you this information. So while you can't dispatch on function types at run-time in general, you can dispatch on function arity. This is what case-lambda does - it makes a function that dispatches based on the number of arguments it receives:

(: dispatcher (case-> [-> Calculate-with-one-number Number Void]
                      [-> Calculate-with-two-numbers Number Number Void]))

(define dispatcher
  (case-lambda
    [([f : Calculate-with-one-number]
      [arg : Number])
     (do-something arg)]
    [([f : Calculate-with-two-numbers]
      [arg1 : Number]
      [arg2 : Number])
     (do-something-else arg1 arg2)]
    [else 42]))