[plt-scheme] typed teaching languages

As so often happens, just after sending this message I realized that I
needed to convince Typed Scheme that real? is a predicate for Number,
so I added

(require/typed scheme [real? (Any -> Boolean : Number)])

at the top, and it now works.

On Sun, Aug 9, 2009 at 6:28 PM, Todd O'Bryan<toddobryan at gmail.com> wrote:
> Thank you. I'm now making progress...
>
> However, I've hit a Typed Scheme hiccup.
>
> (define (positive-real? v)
>  (and (real? v) (>= v 0)))
>
> won't type check because it thinks the second v is just an Any.
>
> I tried adding a type annotation (ann v Number) with a begin around
> the second part of the and, but that didn't help.
>
> Anybody know how to give Typed Scheme the hint it needs here?
>
> Todd
>
> On Sun, Aug 9, 2009 at 2:29 PM, Robby
> Findler<robby at eecs.northwestern.edu> wrote:
>> You probably want
>>
>> (require (for-syntax scheme/base))
>>
>> and then a whole bunch of other changes too :)
>>
>> Robby
>>
>> On Sun, Aug 9, 2009 at 11:21 AM, Todd O'Bryan<toddobryan at gmail.com> wrote:
>>> OK, I've dug into teachprims.ss, but immediately hit a problem.
>>>
>>> I changed the language to
>>>
>>> #lang typed-scheme
>>>
>>> but if I try to run the file, I get an immediate error before I make
>>> anymore changes:
>>>
>>> compile: unbound identifier in the transformer environment (and no
>>> #%app syntax transformer is bound) in: syntax-case
>>>
>>> Does Typed Scheme interact strangely with macros so that I'd have to
>>> unpack all the define-teach definitions in the teachprims file, or am
>>> I just doing something stupid?
>>>
>>> Todd
>>>
>>> On Sat, Aug 8, 2009 at 1:17 PM, Todd O'Bryan<toddobryan at gmail.com> wrote:
>>>> I guess the big problem I'm having dealing with the primitives in
>>>> places like beginner-funs.ss and teachprims.ss is that they use a lot
>>>> of macros--provide-and-document and define-teach--to name two. Is it
>>>> safe to just change the languages in those files to typed-scheme and
>>>> stick in a type annotation, or will that have some kind of weird
>>>> interaction with the macro-provided definitions and the later
>>>> renaming? I really need to get a good handle on macros and I just
>>>> don't have it yet.
>>>>
>>>> I considered trying OCaml, but currying of functions, the lack of
>>>> warnings about function arguments not appearing in application
>>>> positions, and the wealth of other stuff that the teaching languages
>>>> do convinced me it was just a bad idea.
>>>>
>>>> Todd
>>>>
>>>> On Sat, Aug 8, 2009 at 12:22 PM, Matthias Felleisen<matthias at ccs.neu.edu> wrote:
>>>>>
>>>>> The languages are located in collects/lang/htdp*. The primitives come from
>>>>> private/ and are obviously labeled as such. Create copies and introduce type
>>>>> checking at your leisure.
>>>>>
>>>>> ;; ---
>>>>>
>>>>> WARNING: If you really believe that type checking should be an integral part
>>>>> of the first few weeks, you do NOT need to use Typed Scheme for this
>>>>> purpose. The type system of Typed Scheme is designed so that programmers can
>>>>> easily port existing Scheme code, programmed in an idiomatic manner, into a
>>>>> typed setting -- with little more effort than annotating all binding
>>>>> occurrences of variables and fields (aka declarations). It isn't perfect in
>>>>> this manner but it's the best such practical effort out there.
>>>>>
>>>>> Since your programming novices are NOT porting code and you DO NOT wish to
>>>>> program in the specific idioms of Scheme, I recommend that you spare
>>>>> yourself the rather large implementation effort for now and experiment with
>>>>> OCAML instead. The language is quite similar to Scheme but comes with a
>>>>> native type system. (I strongly recommend always using type annotations and
>>>>> to shunt type inference as much as possible.) Use only those constructs that
>>>>> are close to the ones in HtDP teaching languages. While this doesn't give
>>>>> you the teaching languages, it restricts the potential for truly weird
>>>>> syntax errors.
>>>>>
>>>>> ;; ---
>>>>>
>>>>> IN GENERAL, we have not thought through the exact nature of the type system
>>>>> that is appropriate for novice programmers. We do know, however, that we can
>>>>> build a contract system that supports dynamic checking. Doing so will be our
>>>>> next step.
>>>>>
>>>>> The DEIN PROGRAM sister project in Germany (included in the core
>>>>> distribution) has beaten us this time and has already done so. I suspect our
>>>>> solution will be similar to theirs.
>>>>>
>>>>> ;; ---
>>>>>
>>>>> Good luck -- Matthias
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>> On Aug 8, 2009, at 12:05 PM, Todd O'Bryan wrote:
>>>>>
>>>>>> Can somebody explain how the structure of the HtDP teaching languages
>>>>>> works?
>>>>>>
>>>>>> I'm interested in, as an experiment, having my students write type
>>>>>> annotations for their programs, just to see whether it clears up their
>>>>>> type confusions or makes it even harder for them to get things right.
>>>>>> I've received advice from several people stating that this is a bad
>>>>>> idea and that I am going to create a great deal of pain for myself, so
>>>>>> I've been forewarned. Realize, however, that I'll spend probably two
>>>>>> months dealing with simple functions and structures before I ever get
>>>>>> to lists, so the problems of polymorphism that rear their heads so
>>>>>> early in a typical college class won't bother me until Halloween or
>>>>>> so. I'm willing to risk the pain, and I'm even willing to accept the
>>>>>> laughing and pointing that are likely to occur when I give up and tell
>>>>>> everyone that I now accept that this was just a bad idea.
>>>>>>
>>>>>> But I can't even get things to begin to work, because I can't grok how
>>>>>> the teaching languages are structured. How would I go about adding
>>>>>> types and type checking (provided by Typed Scheme) to the language
>>>>>> constructs of Beginning Student? I tried obvious things like changing
>>>>>> scheme/base to typed-scheme in the htdp-beginner files, but I end up
>>>>>> not being able to make the colon type annotation available and when I
>>>>>> try to run programs I get errors saying that there are type
>>>>>> annotations missing.
>>>>>>
>>>>>> David Van Horn provided me with some work he started on in this vein,
>>>>>> but he was working with Advanced Student rather than Beginning and the
>>>>>> internal structure of each of the teaching languages is so complicated
>>>>>> that I can't tell which htdp-advanced's I can just replace with
>>>>>> htdp-beginner's and which ones I have to reconstruct.
>>>>>>
>>>>>> Is there a document anywhere that describes how the teaching languages
>>>>>> are built or is it all just in the code?
>>>>>>
>>>>>> Parenthetically, it's really hard to figure out where things are
>>>>>> coming from as I'm trying to read through Scheme code without running
>>>>>> Check Syntax and using Jump to Definition. Is this the normal state of
>>>>>> Scheme coding or am I missing something that would make figuring out
>>>>>> how the pieces fit together easier?
>>>>>>
>>>>>> Thanks,
>>>>>> Todd
>>>>>> _________________________________________________
>>>>>>  For list-related administrative tasks:
>>>>>>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>>>>>
>>>>>
>>>>
>>> _________________________________________________
>>>  For list-related administrative tasks:
>>>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>>>
>>
>