[Feature Request] let `All` more flexible.

[NoahStoryM]

Automatic matching types for nested All

Code Example

#lang typed/racket/base

(: CONS (All (A) (All (B) [-> A B (Pairof A B)])))
(define CONS (λ (a b) (cons a b)))

(println ((inst CONS Symbol) 'hello " world"))
(println ((inst (inst CONS Symbol) String) 'hello " world"))
(println (CONS 'hello " world"))
(println ((inst CONS Symbol String) 'hello " world"))

Print

'(hello . " world")
'(hello . " world")
'(hello . " world")
'(hello . " world")

Support the use of nested All to separately declare ooo for the parameter type and return value type.

Code Example

#lang typed/racket/base

(: box->list (All (A) [-> (Boxof A) (List A)]))
(define box->list (λ (b) (list (unbox b))))

(: list->box (All (A) [-> (List A) (Boxof A)]))
(define list->box (λ (b) (box (car b))))


(: lists->boxes (All (I ...)
                     (All (O ...)
                          [-> [-> (List  I) ... I (Values (List  O) ... O)]
                              [-> (Boxof I) ... I (Values (Boxof O) ... O)]])))
;; (: lists->boxes (All* (I ...) (O ...)
;;                       [-> [-> (List  I) ... I (Values (List  O) ... O)]
;;                           [-> (Boxof I) ... I (Values (Boxof O) ... O)]]))
(define lists->boxes
  (λ (func)
    (λ boxes
      (call-with-values
       (λ ()  (apply func   (map box->list boxes)))
       (λ res (apply values (map list->box res)))))))

(ann (inst (inst lists->boxes String Symbol) Number Boolean)
     ;; (inst* lists->boxes (Values String Symbol) (Values Number Boolean))
     [-> [-> (List  String) (List  Symbol) (Values (List  Number) (List  Boolean))]
         [-> (Boxof String) (Boxof Symbol) (Values (Boxof Number) (Boxof Boolean))]])

Print

#<procedure:lists->boxes>

[samth]

It seems like there are three things being requested here:

1. Type argument inference for nested All, as in your (CONS 'hello "world") example.
2. Automatic uncurrying of nested All, as in your (inst CONS Symbol String) example.
3. Support for call-with-values with ..., as in the body of lists->boxes.

1 and 3 seem like reasonable things to add, although 3 isn't about All. Changing inst, as described in 2, seems like a less-good idea -- we don't allow the analogous behavior with lambda, and I'm not sure why we would want to add it here.

[NoahStoryM]

Regarding 2., I just think that although the CONS in the first example is defined with nested All, but the use of CONS is very similar to cons, so (inst CONS Symbol String) looks better than (inst (inst CONS Symbol) String), which is more concise.

And I'm not sure whether my understanding of curry is correct: if the programming language supports currying of lambdas, then the ability to check the number of parameters when the function is called is lost.

In the current Typed Racket, the processing of All is like this:

> (:print-type cons)
(All (a b) (case-> (-> a (Listof a) (Listof a)) (-> a b (Pairof a b))))
> (:print-type (inst cons Symbol))
(case->
 (-> Symbol (Listof Symbol) (Listof Symbol))
 (-> Symbol Any (Pairof Symbol Any)))

> (: CONS (All (a b) (-> a b (Pairof a b))))
> (:print-type CONS)
(All (a b) (-> a b (Pairof a b)))
> (:print-type (inst CONS Symbol))
(-> Symbol Any (Pairof Symbol Any))

So when we using inst, there is no need to consider checking the number of parameters of All, and the current TR uses Any to complete the remaining types. So I think why not just currying All?

> (:print-type cons)
(All (a b) (case-> (-> a (Listof a) (Listof a)) (-> a b (Pairof a b))))
> (:print-type (inst cons Symbol))
(case->
 (-> Symbol (Listof Symbol) (Listof Symbol))
 (All (b) (-> Symbol b (Pairof Symbol b))))

> (: CONS (All (a b) (-> a b (Pairof a b))))
> (:print-type CONS)
(All (a b) (-> a b (Pairof a b)))
> (:print-type (inst CONS Symbol))
(All (b) (-> Symbol b (Pairof Symbol b)))

[NoahStoryM]

In current TR, the following code works fine:

> (ann (ann (λ (a) a)
            (∀ (A) (-> (-> A A) (-> A A))))
       (-> (-> String String) (-> String String)))
- : (-> (-> String String) (-> String String))
#<procedure>
> (ann (ann (λ (a) a)
            (∀ (A) (∀ (B) (-> (-> A B) (-> A B)))))
       (∀ (A) (-> (-> A A) (-> A A))))
- : (All (A) (-> (-> A A) (-> A A)))
#<procedure>

But the following code is not possible:

> (ann (ann (λ (a) a)
            (∀ (A) (-> (-> A A) (-> A A))))
       (∀ () (-> (-> String String) (-> String String))))
string:1:10: Type Checker: Error in macro expansion -- Expected 1 type variables, but given 0
  in: (λ (a) a)
 [,bt for context]
> (ann (ann (λ (a) a)
            (∀ (A B) (-> (-> A B) (-> A B))))
       (∀ (A) (-> (-> A A) (-> A A))))
string:1:10: Type Checker: Error in macro expansion -- Expected 2 type variables, but given 1
  in: (λ (a) a)
 [,bt for context]

If TR automatically curries ∀, and treats (∀ () T) as T, we can get more subtyping relations.

In addition, I wonder if it's possible to retain type variables as much as possible when polymorphic data is used as a parameter of a function?

Here's how TR currently behaves:

> (: f (∀ (A B) (-> (-> A B) (-> A B))))
> (define (f x) x)
> (f identity)
- : (-> Nothing Any)
#<procedure:identity>

> (: g (∀ (A) (∀ (B) (-> (-> A B) (-> A B)))))
> (define (g x) x)
> ((ann g (∀ (A) (-> (-> A A) (-> A A)))) identity)
- : (-> Any Any)
#<procedure:identity>
> (g identity)
string:1:0: Type Checker: Cannot apply expression of type (All (A) (All (B) (-> (-> A B) (-> A B)))), since it is not a function type
  in: (g identity)
 [,bt for context]

Here's how I expect TR to behave:

> (: f (∀ (A B) (-> (-> A B) (-> A B))))
> (define (f x) x)
> (f identity)
- : (∀ (A) (-> A A))
#<procedure:identity>

> (: g (∀ (A) (∀ (B) (-> (-> A B) (-> A B)))))
> (define (g x) x)
> ((ann g (∀ (A) (-> (-> A A) (-> A A)))) identity)
- : (∀ (A) (-> A A))
#<procedure:identity>
> (g identity)
- : (∀ (A) (-> A A))
#<procedure:identity>