SHARE
TWEET

Typed Racket filters

a guest Aug 21st, 2012 166 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. #lang typed/racket
  2.  
  3. ;; Typed Racket has some neat tricks
  4. ;; that allow it to type Racket programs.
  5.  
  6. ;; One important trick is that it can pass "filter" information around
  7. ;; in branches of a cond expression,
  8. ;; as well as a few other expressions like cond.
  9.  
  10. ;; Filters tell you additional type information about a value
  11. ;; that you have learned as evidenced by the fact
  12. ;; that you entered a particular branch of a cond (or similar expression).
  13.  
  14. ;; Let's start with a very simple struct:
  15.  
  16. (struct: foo ([val : Integer]))
  17.  
  18. ;; Typed Racket can generate a predicate for any type.
  19. ;; This predicate will not only respond with #t
  20. ;; when the value you give it has that type,
  21. ;; but it also comes with filter information attached,
  22. ;; so if you use it in the test portion of a cond,
  23. ;; it can tell that branch, and any subsequent branches,
  24. ;; whether or not that value has that type.
  25.  
  26. #;(define-predicate foo? foo)
  27. ;; ^ As it happens, struct: will already do this for us.
  28.  
  29. (foo? (foo 3)) ;; => #t
  30. (foo? 3) ;; => #f
  31.  
  32. ;; Filter types are written (: pred? (dom -> rng : t))
  33. ;; I read this as "pred? proves t",
  34. ;; meaning that if a value of type "t" is input,
  35. ;; pred? will return #t
  36.  
  37. ;; the type of foo? is
  38. ;; (: foo? (Any -> Boolean : Foo))
  39.  
  40.  
  41. ;; Filters make racket code well-typed,
  42. ;; because they reflect a programmer's intuition
  43.  
  44. (begin
  45.   ;; suppose we didn't know x's type
  46.   (define: x : Any (foo 3))
  47.   (cond
  48.     ;; we can use foo-val on x in this branch
  49.     ;; because we know x is a foo
  50.     [(foo? x) (foo-val x)]
  51.     ;; however it is a type error to use foo-val in this branch
  52.     ;; because we know x is not a foo
  53.     [else #;(foo-val x) #f]))
  54.  
  55.  
  56. ;; -----------------------------------------------------------
  57.  
  58. ;; Let's define some effective synonyms for foo?
  59. ;; to demonstrate what Typed Racket can do,
  60. ;; and what -- for some odd reason -- it cannot.
  61.  
  62. ;; First, a straightforward (though slightly roundabout) way
  63. ;; of testing the same thing as "foo?" does:
  64.  
  65. (: foo?2 (Any -> Boolean : foo))
  66. (define (foo?2 x)
  67.   (cond
  68.     [(foo? x) #t]
  69.     [else #f]))
  70.  
  71. ;; This works :)
  72.  
  73.  
  74. ;; Ok, now suppose in the #f case
  75. ;; we instead want to throw an exception.
  76.  
  77. ;; (error blah blah) has type Nothing
  78. ;; so we can annotate it to have type False,
  79. ;; since Nothing is a subtype of False.
  80. ;; We'd expect the type system to treat the annotated error
  81. ;; exactly the same as if it were #f
  82.  
  83. #;(: foo?3 (Any -> Boolean : foo))
  84. #;(define (foo?3 x)
  85.   (cond
  86.     [(foo? x) #t]
  87.     [else (ann (error 'foo?3 "wat") False)]))
  88.  
  89. ;; Alas, we get an exception from the type checker.
  90.  
  91. ;; Expected result with filter ((Foo @ x) | (! Foo @ x)),
  92. ;; got filter (Top | (! Foo @ x)) in: (cond ...)
  93.  
  94. ;; Hold on, what???
  95. ;; The branch that returns #t remains unchanged.
  96. ;; The branch that the type system is supposed to believe
  97. ;; returns false is the one that changed.
  98. ;; So wouldn't you expect the (! Foo @ x) portion of the filter
  99. ;; to have changed?
  100.  
  101.  
  102. ;; Ok, well maybe we can fake the type system out
  103. ;; with a thunk to false, which is actually an error.
  104.  
  105. (: wat (-> False))
  106. (define (wat) (error 'wat "wat"))
  107.  
  108. #;(: foo?4 (Any -> Boolean : foo))
  109. #;(define (foo?4 x)
  110.   (cond
  111.     [(foo? x) #t]
  112.     [else (wat)]))
  113.  
  114. ;; Nope, type checker treats this just the same.
  115.  
  116. ;; Expected result with filter ((Foo @ x) | (! Foo @ x)),
  117. ;; got filter (Top | (! Foo @ x)) in: (cond ...)
  118.  
  119.  
  120. ;; Well does it accept *any* synonyms to False?
  121.  
  122. (: wat2 False)
  123. (define wat2 #f)
  124.  
  125. #;(: foo?5 (Any -> Boolean : foo))
  126. #;(define (foo?5 x)
  127.   (cond
  128.     [(foo? x) #t]
  129.     [else wat2]))
  130.  
  131. ;; Nope.
  132.  
  133. ;; Expected result with filter ((Foo @ x) | (! Foo @ x)),
  134. ;; got filter ( (OrFilter (! False @ wat2) (Foo @ x))
  135. ;;            | (AndFilter (False @ wat2) (! Foo @ x)))
  136.  
  137. ;; Well, that's new.
  138. ;; Why does the type system think that wat2 might not be #f,
  139. ;; even though I have already told it that its type is False?
  140. ;; And it is type-restricted to the value False,
  141. ;; it cannot possibly hold any other value.
  142.  
  143.  
  144. ;; Let's try one last time.
  145. ;; Maybe if we bind the #f literal locally
  146. ;; the type system will be ok with it.
  147.  
  148. #;(: foo?6 (Any -> Boolean : foo))
  149. #;(define (foo?6 x)
  150.   (cond
  151.     [(foo? x) #t]
  152.     [else (let: ([its-false-i-promise : False #f])
  153.             its-false-i-promise)]))
  154.  
  155. ;; got filter (Top | (! foo @ x))
  156.  
  157. ;; Sigh. I love the idea of filters,
  158. ;; but is the typechecker so paranoid
  159. ;; that it denies me even the simplest usage of equational reasoning
  160. ;; with regards to value substitution?
RAW Paste Data
Top