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

2011/12/2 Sam Tobin-Hochstadt <samth at ccs.neu.edu>

> 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.
>

It seems so... the biggest problem for now is that either I can't construct
the woven function with the same type as the original one, or I can't apply
it :-p (the problem at the origin of the thread)

I think the weaver should have type (All (A B) ((A -> B) jp aspect-env ->
(A -> B))) and that's what I've been trying to do, unsuccesfully.

Any ideas for a reduced version that might work?

I was thinking of using a union type with a certain subset of types, and
then manually check one-by-one to produce the expected result.

Thanks

-- 
Ismael
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20111202/7db0bd84/attachment.html>