[plt-scheme] HtDP Section 14: stricter typing for eye color?

At Sun, 15 Feb 2004 22:48:53 -0500, Terrence Brannon wrote:
> Comments do not enforce type safety. A comment in a program does not
> prevent me from putting something there that never belongs there,
> perhaps by a typo or some sort of intentional malice.

I am well aware of this. I answered the original poster's message in
the context of How to Design Programs (a textbook for introductory
programming, aka HtDP), which was clearly how it was asked.

> >FWIW, this is one of the clear advantages of Scheme over languages like
> >Pascal -- types can correspond to subsets of other types.
> >
>
> Now you really have me lost: how in the heck is something in a comment 
> going to force the eye-color to only be one of a set of symbols? I am 
> sure you are familar with the concept of an enumerated type. How does 
> one restrict the value for eye color ?

Enforcement is a separate issue from specification. The comments you
saw were only a specification. 

Have a look at this data definition, aka type (again in HtDP notation):

  an xml-expression is:
    - (cons 'symbol list-of-xml-expression

  a list-of-xml-expression is either:
    - '()
    - (cons xml-expression list-of-xml-expression)

As you can see, the constructor (cons) is being used to construct two
different types. This is not possible, for example, in ML or other
typed languages (that's what I was hinting about above). In Scheme,
however, clearly I can write such things down.

Of course, the real question is how to enforce them. For one answer,
see Cormac Flanagan's dissertation (and related papers on MrSpidey). He
uses a set-based analysis to compute a set of values for each program
point and his system can accommodate such types as above.

Robby