[racket] An error with dates and types

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
>