inconvenience in typed Racket

[Hendrik Boom]

Here's the code it's complaining about.

`(,@params -> ,rettype)

And here's the message:

Type Checker: Polymorphic function `qq-append' could not be applied to arguments:
Types: (Listof a) (Listof b) -> (Listof (U a b))
Arguments: (Listof (List Any ': Any)) (List '-> Ffi-type)
Expected result: Ffi-type
in: (quasiquote ((unquote-splicing params) -> (unquote rettype)))

Now what I'm building is a piece of Racket code that is to be written
out into a new source-code file.

param is indeed of type (Listof (List Any ': Any)).
rettype is indeed of type (List '-> Ffi-type)

And or some reason the type-checker isn't able to realise that I can
really build a valid s-expression out of these components.

Now i could hand-expand the quasiquote in to a lot of cons operations,
each presummably surrounded by 'inst' becausee cons is polymorphic,
but this will just make the entire expression unreadable.

I'm almost tempted to write this expression in untyped Racket.

But separating this stuff into another module would significantly
demodularize the code -- related code will no longer be together.

Racket does have a compact mechanism to embed typed-Racket code in an
untyped program (it's called with-type)

But there seems to be no similar way to embed an expression of untyped
code into a typed-racket program.

How to get past this impasse? The majority of my code needs to be in
typed Racket to maintain my sanity while debugging, but the quasiquoted
texts (there are a number of these) need to be readable, for the same
reason.

-- hendrik

[Sam Tobin-Hochstadt]

The problem is almost certainly that `Any` is not allowed in
`Ffi-type`. What's the definition of `Ffi-type`, and why does `params`
have a type that involves `Any`?

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.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/20200522212056.m3x54f6dykgs4qyx%40topoi.pooq.com.

[Hendrik Boom]

On Fri, May 22, 2020 at 05:35:04PM -0400, Sam Tobin-Hochstadt wrote:
> The problem is almost certainly that `Any` is not allowed in
> `Ffi-type`. What's the definition of `Ffi-type`,

Casting rettype to Any did not help; adding Any in as one of the options
in ffi-type did let it go through.


It's completely obscure to me why inserting Any as an additional
alternative in Ffi-type works.

But I don't *want* Any to be a valid alternative for Ffi-type anywhere
else in the program. It will let too much through. I'm adding types to
existing untyped code in an attempt to get some understanding of its
data structures, and using Any here would not teach me anything.

I suppose I could cast rettype to a union Ffi-type and Any in situ.
Ugly.

and why does `params`
> have a type that involves `Any`?

Because it has a lot af possiilities and I haven't yet gotten to
figuring out what's really needed.

I think there's a need to embed untyped expressions in a typed program,
just as there's a mechanism to do the reverse.

-- hendrik

> https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BZah-zmPNKX%3DyttQoQFs7pY9PHc8hYGzkTeKm35YU3MLg%40mail.gmail.com.