Type cases for subtracting 1 from Int>1 producing PosInt

[AlexKnauth]

Refines the types of sub1 and (- _ 1) so that if the argument has a positive integer type known greater than 1, the result of subtraction still has a positive integer type.

This is useful in cases where a function recurs on a positive integer and treats 1 as the base case. In the else case, it's known to not be 1, so the sub1 should be known to be positive:

(define-predicate one? One)
(: pick1 (-> Positive-Integer (Listof Any) Any))
(define (pick1 n lst)
  (cond [(one? n) (car lst)]
        [else (pick1 (sub1 n)
                     (cdr lst))]))

[samth]

This should be easy to do with refinement types. Do we think it's worth adding more cases to the numeric tower for?

[AlexKnauth]

Okay, I see your point, this slight variation passes using #:with-refinements

#lang typed/racket #:with-refinements
(: pick1 (-> Positive-Integer (Listof Any) Any))
(define (pick1 n lst)
  (cond [(= 1 n) (car lst)]
        [else (pick1 (sub1 n)
                     (cdr lst))]))

However, is there a way to make it typecheck by default, without the user having to add #:with-refinements at the top?

[samth]

I'm still skeptical that we should take this route to more precise typechecking of numeric types, rather than using refinements.