That's another good idea: translate provide/contract specs into types.
On Aug 21, 2011, at 6:16 PM, Robby Findler wrote: > Perhaps it would be nice to have require exist in TR but for it to > collaborate with provide/contract to turn the parts of the contracts > that it can into types (and leave behind some contract checking) and, > when you or Ryan or someone figures out how macros & contracts work > together, to fit those into the picture later. > > Robby > > On Sun, Aug 21, 2011 at 4:20 PM, Matthias Felleisen > <matth...@ccs.neu.edu> wrote: >> >> >> The way I understand the word "ought" comes with a moral connotation. >> In this sense, I am saying >> >> (1) require should not exist in TR >> >> (2) require: should exist for importing from typed modules >> >> (3) require-typed should exist for importing from untyped modules. >> >> Why? The idea of explicit specifications is sound/safe *documentation*. >> I consider this aspect particularly important at the boundary between >> typed and untyped code. >> >> What do we lose if we go this route? As far as I can tell, we lose >> the ability to import macros from untyped modules. I consider this >> *good* because macros cause problems with error messages. So what >> we need is a way to require-typed macros (and I have an idea on that). >> >> [[ I honestly didn't know that we could import stuff from untyped >> modules and hope that require could figure out that it types. It >> doesn't even work for >> (module a racket/base (define x 5) (provide x)) >> so I am not sure what we could get to work. ]] >> >> -- Matthias >> >> >> >> >> >> On Aug 21, 2011, at 1:56 PM, Carl Eastlund wrote: >> >>> I still don't follow. There's a shallow error -- 'ought' means the >>> same as 'should', presumably you mean to remove 'be able to' instead. >>> But there's also a deeper error, as far as I can tell. In general, >>> one should use require rather than require/typed so you use a >>> binding's originally assigned type rather than assigning a new one. >>> One shouldn't use require for untyped bindings, but the problem here >>> is that Typed Racket blew up internally before it could report that >>> date->seconds is untyped. >>> >>> Carl Eastlund >>> >>> On Sun, Aug 21, 2011 at 1:47 PM, Matthias Felleisen >>> <matth...@ccs.neu.edu> wrote: >>>> >>>> I should have used 'ought' instead of 'should'. >>>> >>>> On Aug 21, 2011, at 1:38 PM, Carl Eastlund wrote: >>>> >>>>> Plain require works fine in Typed Racket; there's only a problem if TR >>>>> cannot typecheck the resulting code. You normally only need to use >>>>> require/typed to assign types to otherwise-untyped imports. The error >>>>> Norman reported looks like an internal error in TR related to the >>>>> contract on date->seconds. Using require/typed is a workaround >>>>> because it avoids typechecking contract-wrapped references. >>>>> >>>>> Carl Eastlund >>>>> >>>>> On Sun, Aug 21, 2011 at 1:16 PM, Matthias Felleisen >>>>> <matth...@ccs.neu.edu> wrote: >>>>>> >>>>>> You shouldn't be able to use plain require in Typed Racket. >>>>>> >>>>>> Try this: >>>>>> >>>>>> #lang typed/racket >>>>>> (require/typed racket/date (date->seconds (date -> Natural))) >>>>>> (date->seconds (seconds->date (current-seconds))) >>>>>> >>>>>> >>>>>> On Aug 21, 2011, at 11:06 AM, Norman Gray wrote: >>>>>> >>>>>>> >>>>>>> Greetings. >>>>>>> >>>>>>> Another typed-racket problem, I'm afraid. >>>>>>> >>>>>>> With the following script, I get an error message from Typed Racket >>>>>>> which is not, I think, really addressed to me. >>>>>>> >>>>>>> (Is the list generally OK for straight bug reports? There isn't a bug >>>>>>> parade I should be posting this on, is there?) >>>>>>> >>>>>>> All the best, >>>>>>> >>>>>>> Norman >>>>>>> >>>>>>> >>>>>>> % cat dates.rkt >>>>>>> #lang typed/racket >>>>>>> (require (only-in racket/date date->seconds)) >>>>>>> (date->seconds (seconds->date (current-seconds))) >>>>>>> % "/Data/LocalApplications/Racket/5.1.3/bin/racket" dates.rkt >>>>>>> for: expected a sequence for i, got something else: (tc-results (list >>>>>>> (tc-result Variable-Reference (#0=Top | #0#) -)) #f) >>>>>>> >>>>>>> === context === >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/racket/private/for.rkt:445:2: >>>>>>> make-sequence >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/typed-scheme/types/utils.rkt:103:2: >>>>>>> ret >>>>>>> temp871 >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/typed-scheme/typecheck/tc-expr-unit.rkt:201:4: >>>>>>> loop >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/racket/private/map.rkt:18:11: >>>>>>> map >>>>>>> parse-loop1141 >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/typed-scheme/typecheck/tc-expr-unit.rkt:330:0: >>>>>>> tc-expr >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/racket/private/map.rkt:18:11: >>>>>>> map >>>>>>> temp971 >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/typed-scheme/typecheck/tc-expr-unit.rkt:330:0: >>>>>>> tc-expr >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/racket/private/map.rkt:18:11: >>>>>>> map >>>>>>> temp971 >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/typed-scheme/typecheck/tc-expr-unit.rkt:330:0: >>>>>>> tc-expr >>>>>>> parse-loop26 >>>>>>> dots-loop >>>>>>> /Data/LocalApplications/Racket/5.1.3/collects/racket/private/map.rkt:18:11: >>>>>>> map >>>>>>> ... >>>>>>> >>>>>>> % >>>>>>> >>>>>>> >>>>>>> -- >>>>>>> Norman Gray : http://nxg.me.uk >>>>>>> School of Physics and Astronomy, University of Glasgow, UK >> >> >> _________________________________________________ >> For list-related administrative tasks: >> http://lists.racket-lang.org/listinfo/users >> _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
