# Managing \`cast\` performance penalty **URL:** \ **Category:** Questions & Answers\ **Tags:** question, typed-racket\ **Created:** [April 21, 2022, 2:22pm UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905 "2022-04-21T14:22:24Z")\ **Posts on this page:** 7\ **Page:** 2
**Author:** ![samth](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/samth/32/3_2.png) [@samth](https://racket.discourse.group/u/samth)\ **Post date:** [April 26, 2022, 5:51pm UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905/21 "2022-04-26T17:51:16Z")
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: ```scheme (: 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. ---
**Author:** ![NoahStoryM](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/noahstorym/32/17_2.png) [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)\ **Post date:** [April 27, 2022, 2:01am UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905/22 "2022-04-27T02:01:04Z")
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`: ```scheme 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? ---
**Author:** ![samth](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/samth/32/3_2.png) [@samth](https://racket.discourse.group/u/samth)\ **Post date:** [April 27, 2022, 4:10am UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905/23 "2022-04-27T04:10:35Z")
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. ---
**Author:** ![NoahStoryM](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/noahstorym/32/17_2.png) [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)\ **Post date:** [April 27, 2022, 4:42am UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905/24 "2022-04-27T04:42:02Z")
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? ---
**Author:** ![samth](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/samth/32/3_2.png) [@samth](https://racket.discourse.group/u/samth)\ **Post date:** [April 27, 2022, 4:55am UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905/25 "2022-04-27T04:55:24Z")
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: ```scheme (: 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: ```scheme (: andmap1 (All (A) (-> (Listof Any) (pred A) Boolean : #:+ (Listof A) #:- (! (Listof A))))) ``` ---
**Author:** ![NoahStoryM](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/noahstorym/32/17_2.png) [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)\ **Post date:** [April 27, 2022, 4:59am UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905/26 "2022-04-27T04:59:36Z")
I think I get it now, thanks a lot for your help! ---
**Author:** ![ben\_greenman](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ben_greenman/32/632_2.png) [@ben\_greenman](https://racket.discourse.group/u/ben_greenman)\ **Post date:** [June 14, 2022, 12:04am UTC](https://racket.discourse.group/t/managing-cast-performance-penalty/905/27 "2022-06-14T00:04:23Z")
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](https://github.com/racket/typed-racket/pull/948) [Previous page](https://racket.discourse.group/t/managing-cast-performance-penalty/905.md?page=1)