Predicates Type for Function Types in Typed / Racket

Question

I am in the early stages of developing a framework and fooling myself 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 sends by 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 to create predicates like Calculate-with-one-number? and Calculate-with-two-numbers? in typed/racket ? For non-functional predicates, I can use define-predicate . But it is unclear how to implement predicates for function types.

Answer 1

Since I myself answer, I take the liberty of clarifying the essence of my question in the light of a discussion of essence as a solution. The difference in essence was due to the fact that I did not consider its consequences when asking a question.

Problem

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

By default, #lang racket executes arity procedures, and any additional specificity in the argument types must be executed 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 of "concluded contracts".

Math as an example

The Typed Racket Guide provides an example using define-type to determine the type of procedure:

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

This allows a more detailed description of the procedure:

  ;; Takes two numbers, returns a number (define-type 2NN (-> Number Number Number)) (: trigFunction1 2NN) (define (trigFunction1 xs) (* s (cos x))) (: quadraticFunction1 2NN) (define (quadraticFunction1 xb) (let ((x1 x)) (+ b (* x1 x1)))) 

goal

In a field such as mathematics, it would be nice to work with more abstract types of procedures, because knowing that the function is cyclical between the upper and lower bounds (e.g. cos ) compared to a single boundary (e.g. our quadratic function) is asymptotic (e.g., hyperbolic function) provides a clearer discussion of the problem area. It would be nice to have access to abstractions, for example:

  (define-type Cyclic2NN (-> Number Number Number)) (define-type SingleBound2NN (-> Number Number Number)) (: trigFunction1 Cyclic2NN) (define (trigFunction1 xs) (* s (cos x))) (: quadraticFunction1 SingleBound2NN) (define (quadraticFunction1 xb) (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 detail when it comes to procedures. Moreover, the brief false hope that we can easily unscrew this type difference for procedures manually using define-predicate breaks down into:

Computes a predicate of type t with type (Any → Boolean: t). t cannot contain function types or types that can refer to mutable data, such as (Vectorof Integer).

In principle, types are used outside of static validation and contracts. As first-class members of the language, we want to be able to send our more subtle types of procedures. It is clear that we need predicates along the lines of Cyclic2NN? and SingleBound2NN? . Not easy enough to send with case-lambda .

Untyped Racket Guide

Fortunately, Lisps are domain-specific languages ​​for writing Lisps, when we return the curtain to open the wizard, and in the end we can get what we want. The key is to solve the problem in another way and ask: "How canwe use typed/racket predicates gives us procedures?"

Structures are data types defined by the Racket user and are the basis for an extension of the type system. Structures are so powerful that even in the class' object system, classes and objects are implemented in terms of structure types .

In #lang racket structures can be used as procedures that expose the #:property keyword using prop:procedure followed by a procedure for its value. The documentation contains two examples:

The first example defines the structure field to be used as a procedure. Obviously, at least once this has been indicated, this field should contain a value that is evaluated by the 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, the anonymous procedure [lambda] is provided directly as part of the property value. The lambda accepts the operand in the first position, which is allowed for the value of the structure used as a procedure. This allows you to access any value stored in any field of the structure, including those evaluated by 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 a typed / racket

Alas, no syntax works with struct , as implemented in typed/racket . The problem is that the static type of verification, as currently implemented, cannot simultaneously determine the structure and allow its signature as a procedure at the same time. The correct information does not appear to be available in the correct phase when using the special form typed/racket struct .

To get around this, typed/racket provides define-struct/exec , which roughly corresponds to the second syntax of #lang racket less than 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. Awakening e is used as a value for the prop: procedure and must be of type proc-t.

This not only gives us strongly typed procedural forms, but also a little more elegantly than the keyword syntax found in #lang racket . The sample code to resolve the question that was given in this answer is as follows:

 #lang typed/racket (define-type 2NN (-> Number Number Number)) (define-struct/exec Cyclic2NN ((f : 2NN)) ((lambda(self xs) ((Cyclic2NN-f self) xs)) : (-> Cyclic2NN Number Number Number))) (define-struct/exec SingleBound2NN ((f : 2NN)) ((lambda(self xs) ((SingleBound2NN-f self) xs)) : (-> SingleBound2NN Number Number Number))) (define trigFunction1 (Cyclic2NN (lambda(xs) (* s (cos x))))) (define quadraticFunction1 (SingleBound2NN (lambda (xb) (let ((x1 x)) (+ b (* x1 x1))))) 

Certain procedures are strictly typified in the sense that:

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

It remains only to write a macro to simplify the specification.

Answer 2

In general, what you want is not possible due to the way the types are implemented in Racket. Racket has contracts that are run-time shells that protect parts of the program from other parts. A function contract is a shell that treats a function as a black box - a form contract (-> number? number?) Can wrap any function, and a new shell function will first verify that it receives one number? and then passes it to the wrapped function, then checks that the wrapped function returns number? . All this is done dynamically every time a function is called. Typed Racket adds the concept of types that are statically checked, but since they can provide and require values ​​from and unexplored modules, these values ​​are protected by contracts that represent their type.

In your dispatcher function, you dynamically take the function f at runtime, and then want to do something based on what function you got. But the functions - black boxes - contracts do not really know anything about the functions that they wrap, they just check that they are behaving correctly. It is impossible to say whether the form function (-> number? number?) Or the form function (-> string? string?) Was specified by the dispatcher . Because dispatcher can accept any possible function, functions are black boxes with no information about what they accept or promise. dispatcher can only assume that the function is correct with the contract and is trying to use it. This is why define-type does not automatically create a predicate for function types - there is no way to prove that a function has a type dynamically, you can only wrap it in a contract and assume that it behaves.

The exception is arity information - all functions know how many arguments they take. The procedure-arity function procedure-arity provide you with this information. That way, although you cannot send function types at run time in general, you can send arity functions. This is what case-lambda does - it executes a function that sends 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]))