[racket] Typed Racket: problem with interaction between typed/untyped modules

On Fri, Dec 2, 2011 at 6:26 PM, Ismael Figueroa Palet
<ifigueroap at gmail.com> wrote:
> Sam, first I want to thank you for all your answers, you've helped me a lot.
> Thanks!
>
>> > I'm trying to implement a function wrapper, that given any function
>> > returns
>> > a function of the same type, but that maybe applies a different
>> > argument. So
>> > far I haven't been successful, and based on previous questions to the
>> > mail
>> > list it seemed that I needed to go to an untyped module because I
>> > couldn't
>> > constraint values to a given type.
>>
>> In general, I don't think that any solution is going to work here.
>> You can't take arbitrary functions and apply them to specific
>> arguments (such as the string "blabla") in a type-safe way.
>
>
> For what I know, the design goal of Typed Racket is to avoid all runtime
> errors. Maybe that is too strict for programs like the one I intend to make.
> The idea of proposing a cast operation is to be able to establish a tradeoff
> between type safety and expressive power, according to the programmer needs.
>
>>
>> In you particular example, the function `f' is a constant function.
>> But what if it expected `Integer' as its argument?  Then your untyped
>> code would be violating the type invariants.
>
>
> I think in that case a contract violation error should happen (?)
>
>>
>>
>> However, you can make your program work just by removing the
>> parameterization over `A', and replacing that with `Any'.  Then your
>> program is safe, and your untyped module can safely call the function
>> with any value it wants.
>
>
> In that case, my program can only work with values of type Any, and I'd need
> to make all functions Any -> (T Any) since I can't downcast to any other
> type, but since I'm passing functions as arguments I will have the problem
> of subtyping between functions...
>
>> As an additional note, the `CAST' operation you describe below, can't
>> do exactly what you expect, because it's runtime semantics depends on
>> how you instantiate `B'.  But that would mean that you'd have to
>> generate code for the `CAST' without knowing what `B' is.
>
>
> do you think it can work if I do (CAST f (Integer -> Boolean)) instead?

Yes, this could work.  I haven't added `cast' yet, but I'll try to do that soon.

> Maybe the flaw in my reasoning is that I think that when you evaluate the
> polymorphic function, then you know what A and B are... so you should be
> able to cast a value to B, is not that so?
>
> is it that you statically prove that the body is OK for all A and B and then
> you don't get that information when applying??

Yes, this latter description is how Typed Racket works.

>>
>> Typed
>> Racket, like ML or Haskell, doesn't pass type parameters around as
>> values, so you can't do this.
>
>
> I don't know much about how the type system of ML or Haskell works.
>
> What I'm trying to do, so you get the full picture, is to write a variation
> of Aspect Scheme in Typed Racket, so you can statically check that advice is
> well-typed. I couldn't type correctly the weaver function, so I tried with
> an untyped module. Maybe it is not possible at all??

That sounds neat.  However, I'm suspicious that you won't be able to
type check everything that people currently write in Aspect Scheme
without changing some part of Typed Racket to understand your system
better.
-- 
sam th
samth at ccs.neu.edu