[racket] error : Attempted to use a higher-order value passed as `Any` in untyped code:

[mailoo]

Hello,

I'm new to racket, and even more with typed/racket.

I play a little with the "Any" type (due to 'dynamic-require' which
return Any), and I'm not able to cast them back in a function.

I (over) simplify my question with this little program :

```
(: p Any)
(define (p i) (displayln i))

; Here I want to get back my function
(define proc (cast p (-> Integer Void)))
(proc 2)

```

but I get this error when I try to execute the function :

```
; contract violation
; Attempted to use a higher-order value passed as `Any` in untyped
code: #<procedure:p>
; in: Any
; contract from: typed-world
; blaming: cast
; (assuming the contract is correct)
; at: <pkgs>/racketFBP/test.rkt:13.13
; Context:
; /home/denis/dev/racket/racketFBP/test.rkt:1:1 [running body]
; [Due to errors, REPL is just module language, requires, and stub
definitions]
```

In reality, I get my function by `(dynamic-require path 'p)`, and I
didn't find a typed version of this function...

Is there a way to go from Any to a function, or to replace my use of
`dynamic-require`?

Thank you in advance,
Denis Michiels

[Matthias Felleisen]

Have you considered organizing your program as follows: 

#lang racket

(module a racket
  (provide f)
  (define (f x) 10))

(module b racket
  (provide g)
  (define g (dynamic-require '(submod "foo.rkt" a) 'f)))

(module c typed/racket
  (require/typed (submod ".." b) [g (-> Integer Integer)])
  (g 20))

(require 'c)

That is, run the dynamic-require in an untyped module and then import it at the desired type? 

-- 
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...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Greg Hendershott]

Maybe do you want `require/typed`?

See:

https://docs.racket-lang.org/ts-guide/typed-untyped-interaction.html#%28part._.Using_.Untyped_.Code_from_.Typed_.Code%29

[mailoo]

Hello,

First thank Greg and Mathias for looking at my problem.

And yes, the proposed solution is working! I didn't think at all by
putting a "module in the middle", to by-pass my cast operation.

Thank you!
Denis

On 04/16/2018 04:01 PM, Matthias Felleisen wrote:
>
> Have you considered organizing your program as follows:
>
> #lang racket
>
> (module a racket
>   (provide f)
>   (define (f x) 10))
>
> (module b racket
>   (provide g)
>   (define g (dynamic-require '(submod "foo.rkt" a) 'f)))
>
> (module c typed/racket
>   (require/typed (submod ".." b) [g (-> Integer Integer)])
>   (g 20))
>
> (require 'c)
>
> That is, run the dynamic-require in an untyped module and then import it
> at the desired type?
>
>
>
>> On Apr 16, 2018, at 5:22 AM, mailoo <dmic...@mailoo.org

>> <mailto:racket-users...@googlegroups.com>.

[Alex Knauth]

This is interesting. The `Any` type in Typed Racket includes values that may have higher-order "original" types. For example, it may have originally been a typed function (-> Fixnum Fixnum) or (-> String Boolean), such that if you call it without a contract guarding it, it should be an error. This is because `Any` is a super type of those types.

However, the value returned by `dynamic-require` is different from a normal `Any`. It will never be an unguarded "originally" typed value, so it should be safe to pass it to `cast` without adding a new guard. It might make sense to define a new type `UntypedAny` or maybe `GuardedAny`. There are two differences:

  (1) this type is *not* a super type of any other type that might involve higher-order values

  (2) it is safe to pass a value of this type into untyped code without an additional guard

Point (2) is what would allow `cast` to work, and point (1) is what would make that safe to do.

With this new `UntypedAny` type, dynamic-require could return the type `UntypedAny` instead of `Any`.

--------------------------------------------------

Why this would allow `cast` to work (and why `require/typed` is a good workaround for now)

The difference between `cast` and `require/typed` is this:

 - `require/typed` guards value going from Untyped -> Typed

 - `cast` guards values going from Typed -> Untyped -> Typed

The `cast` needs the extra Typed -> Untyped boundary to guard "originally" typed higher-order values, such as a (-> Fixnum Fixnum) function annotated as `Any`. However, `require/typed` takes its values from an untyped context to begin with, so it doesn't need to deal with that extra boundary.

The value returned by `dynamic-require` is never one of those typed higher-order values, and if the type system knows that through the `UntypedAny` type, the type system will know it is safe to make `cast` behave like `require/typed`.

It will know it is safe to pass it only through the Untyped -> Typed boundary.

Alex Knauth

[mailoo]

Hello,

I continue my work with Typed/Racket and Racket, and I now have another problem, with the same error.

I try to use in untyped racket a typed async-channel of type Any, and I'm not able to use the higher-order value from this channel.
Here is an example code that show this problem :

```
#lang racket

; A higher-order value
(define add (lambda (x) (+ x 1)))
(add 1)

; Untyped is working well
(require racket/async-channel)
(define untype-p (make-async-channel 10))
(async-channel-put untype-p add)
(define new-add (async-channel-get untype-p))
(display "untype world : ")
(displayln (new-add 2))

; Untype <-> type world doesn't work
(module port typed/racket
(provide build-port (struct-out port))

(require typed/racket/async-channel)

(struct port ([channel : (Async-Channelof Any)]))

(: build-port (-> port))
(define (build-port)
(port (make-async-channel 10))))

(require 'port)
(define p (build-port))

(async-channel-put (port-channel p) add)
(define n-add (async-channel-get (port-channel p)))

; Fail : Attempted to use a higher-order value passed as `Any` in untyped code: #<procedure:add>
(n-add 3)
```

Do you have an idea how I can use my procedure?
I don't know if it's possible, or if it is a limitation of the untyped <-> typed boundary?

[mailoo]

Unfortunatly, not.
I'm building a framework were the user will send data over the
async-channel, so I didn't know the type in advance, and cannot specify
more the async-channel...

On 04/20/2018 02:50 PM, Sam Tobin-Hochstadt wrote:
> Can you give a more specific type to what you send on the channel? That
> will allow Typed Racket to generate a contract that works for your values.
>
> Sam

> --
> 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...@googlegroups.com

> <mailto:racket-users%2Bunsu...@googlegroups.com>.

[Matthias Felleisen]

Can you move the communication into an untyped submodule and use external type specs to move the values into the typed world? We could learn from this what’s missing from Typed Racket.

> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.

[Sam Tobin-Hochstadt]

In that case, which side is not typed? If the user side isn't typed,
then you can _read_ things of type `Any` from the channel just fine.

Sam

> email to racket-users...@googlegroups.com.

[mailoo]

The untyped world will read and write... The typed world surround this
actions (async-channel-put and async-channel-get) by other things.

I want my framework Typed and using it untyped, but it seems hard to manage!

But beside, thank you for looking at my problem!

[stewart mackenzie]

Probably better to revert back to untyped racket for the meantime...