[plt-scheme] typed teaching languages

From: Todd O'Bryan (toddobryan at gmail.com)
Date: Sun Aug 9 18:28:58 EDT 2009

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?


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

Posted on the users mailing list.