[racket] An error with dates and types

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
> <matthias at 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
>>> <matthias at 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
>>>>> <matthias at 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
>>