No, this isn't a bug. The problem is the cast _from_ `Any`, which
means we can't know what kind of value we have or how to protect it
more than we do.

This isn't introducing runtime errors into correct programs any more
than this one is:

#lang typed/racket
(: id : (-> String String))
(define (id x) x)
((cast id (-> Boolean Boolean))  #t)

which will also error.

Higher-order contracts are always potentially "time bombs" in this
sense, because they delay checking.

Sam


On Thu, Feb 16, 2017 at 3:15 PM, John Clements
<cleme...@brinckerhoff.org> wrote:
> Here’s a simple program that fails:
>
> #lang typed/racket
>
> (define (obscurinator [x : Any]) : Any
>   x)
>
> (struct PrimV ([f : (Real Real -> Real)]) #:transparent)
>
> (define dangerval : PrimV
>   (cast (obscurinator (PrimV +))
>         PrimV))
>
> ((PrimV-f dangerval) 3 4)
>
> It type-checks fine, but it produces this error in 6.8.0.2--2017-01-19(-/f) 
> [3m].:
>
> contract violation
>   Attempted to use a higher-order value passed as `Any` in untyped code: 
> #<procedure:+>
>   in: Any
>   contract from: typed-world
>   blaming: cast
>    (assuming the contract is correct)
>   at: unsaved-editor:9.2
>
> Basically, the ‘cast’ to a higher-order value type creates a time bomb that 
> blows up when called. Is this a bug?
>
> More generally, how do we feel about a type system that appears to introduce 
> run-time errors into otherwise correct programs? I think it might be nicer 
> just to prevent casts to higher-order types than to introduce this kind of 
> time bomb (pardon the excessively pejorative term). Apologies if I’m 
> misunderstanding this. Or maybe this is a fixable bug in TR?
>
> At a minimum, explaining it to a class of Java programmers is going to be 
> interesting.
>
> John
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Reply via email to