Hi all,
I've been following HtDP to teach introductory programming at USI Lugano for several years now, and I really like the approach. The one thing that I have been missing from the student languages is some kind of support for type annotations, so as to be able to turn the data type definitions that are so central to HtDP's approach into something that is more than comments with (structured) natural language.
Recently, I actually found out that something like that has been available since Racket 8.9 (!), in the form of checked signatures. This is great: I definitely intend to integrate it in my teaching material and let the students systematically use these features.
While trying out checked signatures, and thinking how to apply them to the various topics of HtDP, I also found a few scenarios where it'd be helpful to have some additional features. I would like to discuss here whether others think these features could be generally useful, and whether they could even be considered for inclusion in the student languages.
Of course, any comments are welcome.
1. Alias mixed as one-of
Function mixed describes mixed data or, as they are sometimes
called in HtDP, itemizations:
(define StringOrInteger (signature (mixed String Integer)))
An itemization is usually described in HtDP with the structured
natural language form:
A StringOrInteger is one of:
- a String
- an Integer
Having one-of as a synonym of mixed would help make formal type
declarations closer to the structured natural language form used in
HtDP:
(define (StringOrInteger (signature (one-of String Integer))
2. Signature definitions without signature
We can use define to give a signature form a name:
(define WeekDay (signature (enum "Mon" "Tue" "Wed" "Thu" "Fry" "Sat" "Sun")))
Since such definitions correspond to data (type) definitions in HtDP,
it would be convenient to have a variant of define that does not
need an explicit signature. Thus, the above definition could be
written as:
(define-type WeekDay (enum "Mon" "Tue" "Wed" "Thu" "Fry" "Sat" "Sun"))
3. Predicate types in BSL
Function predicate allows one to define a type constrained by a
predicate, which returns #true precisely for the values that belong
to the type.
(define (nonzero-number? v) (and (number? v) (not (= v 0))))
(define NonZeroNumber (signature (predicate nonzero-number?)))
Even though predicate is defined in all student languages, it cannot
really be used in BSL or BSL+ where functions are not first class.
I'm unsure what's the best way of handling this. Removing predicate
from BSL is not a good idea, given that there are several examples of
data type definitions that are already used with BSL and BSL+ (e.g.,
interval data types in HtDP) but would require predicate to be
defined.
4. Posn and PosnOf
A define-struct with name struct also defines signature forms
Struct and StructOf. For example:
(define-struct name [first last])
; name-full inputs instances of `name` where both fields are strings
(: name-full ((NameOf String String) -> String))
(define (name-full n) (string-append (name-first n) " " (name-last n)))
; the constructor of `name` returns an instance of type `Name`
(: make-name (Any Any -> Name))
In the student languages, there is a predefined struct called
posn. However, the type names Posn and PosnOf are not defined.
5. Support type-annotated struct definitions
Often one wants to constrain the types of fields in a struct. This
is possible by providing a signature for the struct's constructor:
(define-struct name [first last])
(: make-name (String String -> (NameOf String String)))
While this works, Name would still refer to a struct with two
fields of any type, whereas the type NameOf String String denotes
the "constrained" type with two strings as fields.
It would be convenient if one could add type constraints to the fields
of a define-struct form, or anyway having a mechanism to easily
define a struct with certain type constraints on its fields.