Typed Racket filters

#lang typed/racket

;; Typed Racket has some neat tricks
;; that allow it to type Racket programs.

;; One important trick is that it can pass "filter" information around
;; in branches of a cond expression,
;; as well as a few other expressions like cond.

;; Filters tell you additional type information about a value
;; that you have learned as evidenced by the fact
;; that you entered a particular branch of a cond (or similar expression).

;; Let's start with a very simple struct:

(struct: foo ([val : Integer]))

;; Typed Racket can generate a predicate for any type.
;; This predicate will not only respond with #t
;; when the value you give it has that type,
;; but it also comes with filter information attached,
;; so if you use it in the test portion of a cond,
;; it can tell that branch, and any subsequent branches,
;; whether or not that value has that type.

#;(define-predicate foo? foo)
;; ^ As it happens, struct: will already do this for us.

(foo? (foo 3)) ;; => #t
(foo? 3) ;; => #f

;; Filter types are written (: pred? (dom -> rng : t))
;; I read this as "pred? proves t",
;; meaning that if a value of type "t" is input,
;; pred? will return #t

;; the type of foo? is
;; (: foo? (Any -> Boolean : Foo))


;; Filters make racket code well-typed,
;; because they reflect a programmer's intuition

(begin
  ;; suppose we didn't know x's type
  (define: x : Any (foo 3))
  (cond
    ;; we can use foo-val on x in this branch
    ;; because we know x is a foo
    [(foo? x) (foo-val x)]
    ;; however it is a type error to use foo-val in this branch
    ;; because we know x is not a foo
    [else #;(foo-val x) #f]))


;; -----------------------------------------------------------

;; Let's define some effective synonyms for foo?
;; to demonstrate what Typed Racket can do,
;; and what -- for some odd reason -- it cannot.

;; First, a straightforward (though slightly roundabout) way
;; of testing the same thing as "foo?" does:

(: foo?2 (Any -> Boolean : foo))
(define (foo?2 x)
  (cond
    [(foo? x) #t]
    [else #f]))

;; This works :)


;; Ok, now suppose in the #f case
;; we instead want to throw an exception.

;; (error blah blah) has type Nothing
;; so we can annotate it to have type False,
;; since Nothing is a subtype of False.
;; We'd expect the type system to treat the annotated error
;; exactly the same as if it were #f

#;(: foo?3 (Any -> Boolean : foo))
#;(define (foo?3 x)
  (cond
    [(foo? x) #t]
    [else (ann (error 'foo?3 "wat") False)]))

;; Alas, we get an exception from the type checker.

;; Expected result with filter ((Foo @ x) | (! Foo @ x)),
;; got filter (Top | (! Foo @ x)) in: (cond ...)

;; Hold on, what???
;; The branch that returns #t remains unchanged.
;; The branch that the type system is supposed to believe
;; returns false is the one that changed.
;; So wouldn't you expect the (! Foo @ x) portion of the filter
;; to have changed?


;; Ok, well maybe we can fake the type system out
;; with a thunk to false, which is actually an error.

(: wat (-> False))
(define (wat) (error 'wat "wat"))

#;(: foo?4 (Any -> Boolean : foo))
#;(define (foo?4 x)
  (cond
    [(foo? x) #t]
    [else (wat)]))

;; Nope, type checker treats this just the same.

;; Expected result with filter ((Foo @ x) | (! Foo @ x)),
;; got filter (Top | (! Foo @ x)) in: (cond ...)


;; Well does it accept *any* synonyms to False?

(: wat2 False)
(define wat2 #f)

#;(: foo?5 (Any -> Boolean : foo))
#;(define (foo?5 x)
  (cond
    [(foo? x) #t]
    [else wat2]))

;; Nope.

;; Expected result with filter ((Foo @ x) | (! Foo @ x)),
;; got filter ( (OrFilter (! False @ wat2) (Foo @ x))
;;            | (AndFilter (False @ wat2) (! Foo @ x)))

;; Well, that's new.
;; Why does the type system think that wat2 might not be #f,
;; even though I have already told it that its type is False?
;; And it is type-restricted to the value False,
;; it cannot possibly hold any other value.


;; Let's try one last time.
;; Maybe if we bind the #f literal locally
;; the type system will be ok with it.

#;(: foo?6 (Any -> Boolean : foo))
#;(define (foo?6 x)
  (cond
    [(foo? x) #t]
    [else (let: ([its-false-i-promise : False #f])
            its-false-i-promise)]))

;; got filter (Top | (! foo @ x))

;; Sigh. I love the idea of filters,
;; but is the typechecker so paranoid
;; that it denies me even the simplest usage of equational reasoning
;; with regards to value substitution?