Managing `cast` performance penalty

Questions & Answers
,
21

  1. The issue with andmap is that it requires a little too much of the predicate, in particular that it have the type (Any -> Boolean : T), which says not only that true results are in T but that false results are not in T. This could be fixed.

  2. Here's a definition of andmap with a less-restrictive type which makes @jbclements's program work:

(: andmap2 (All (A) (Any -> Boolean : #:+ A) (Listof Any) -> Boolean : #:+ ((Listof A) @ 1)))
(define (andmap2 f l)
  (cond [(empty? l) #t]
        [(f (car l)) ((inst andmap2 A) f (cdr l))]
        [else #f]))
  1. I strongly discourage using unsafe for experimenting with the type system, since it makes it easy to think something is right when it doesn't work.
5 Likes
22

Thanks for your reminder! I didn't have a very clear understanding of the dangers of unsafe before. I will use it with caution. (I guess maybe I should use unsafe when require/typed doesn't work, or when I don't know how to properly define a function in TR?).

I'm not very clear about the usage of proposition in ->. I'd like to know what does @ mean and how to use it?

In addition, I still have some doubts about the use of andmap. I tried to define listof? through my own andmap1:

Welcome to Racket v8.4 [cs].
> (: andmap1 (All (A) [-> (pred A) (Listof Any) Boolean]))
> (define andmap1
    (λ (pred ls)
      (or (null? ls)
          (and (pred (car ls))
               ((inst andmap1 A) pred (cdr ls))))))
> (: listof? (All (A) [-> (pred A) (pred (Listof A))]))
> (define listof?
    (λ (pred)
      (λ (arg)
        (and (list? arg)
             ((inst andmap1 A) pred arg)))))
string:5:11: Type Checker: type mismatch;
 mismatch in proposition
  expected: ((: arg (Listof A)) | (! arg (Listof A)))
  given: (Top | Top)
  in: ((inst andmap1 A) pred arg)
 [,bt for context]
>

It shows that andmap1 cannot be used like andmap (I guessed it was a type problem, so I retyped the type of andmap by unsafe-require/typed before), I wonder how to define andmap1 correctly?

23

On unsafe: Typed Racket is really just believing you that it will work, so anything you write will be accepted. It's thus easy to get total nonsense.

The problem with your andmap1 is that it doesn't have a proposition, which is what's important about the built-in andmap and my andmap2.

My definition of andmap2 is almost exactly like yours, so I'm not sure what you're asking. That is exactly how I would define it.

1 Like
24

I'm confused by these questions:

  1. what the @ in -> means and how should I use it? (I didn't find an introduction to it from the document, did I miss something?)
  2. I want to define andmap1 which behaves the same as the built-in andmap (it is not strictly required that the argument type must be (-> a c : d), and the non-predicate case is not considered, so only the (pred d) type is considered), what should I do? (I'm not sure if andmap2 meets it, I don't understand its proposition).
  3. Can we retype the built-in andmap with more precise one?
25

Out of order:

  1. Yes, we just need a small patch to the type of andmap.
  1. @ says which argument the proposition refers to. So in ((Any -> Boolean : #:+ A) (Listof Any) -> Boolean : #:+ ((Listof A) @ 1) the proposition says that the second argument (indexes start at 0) is a (Listof A) if the result is not-#f.
  2. To just redefine the simple, two argument version of andmap1 you would give it this type:
(: andmap1 (All (A) (pred A) (Listof Any) -> Boolean : #:+ ((Listof A) @ 1) #:- (! (Listof A) @ 1)))

The type is complicated because it refers to the second argument. If you flip the arguments you can use the simpler type:

(: andmap1 (All (A) (-> (Listof Any) (pred A) Boolean : #:+ (Listof A) #:- (! (Listof A)))))
1 Like
26

I think I get it now, thanks a lot for your help!

27

At long last, Shallow & Optional Typed Racket are about ready to merge.

Reviews, comments, and questions welcome: transient semantics by bennn · Pull Request #948 · racket/typed-racket · GitHub

10 Likes