[plt-scheme] typed teaching languages

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