[plt-scheme] The perfect teaching language--Is this too much to ask for?

On Sat, Jun 13, 2009 at 7:36 PM, Matthias Felleisen<matthias at ccs.neu.edu> wrote:
>
> On Jun 13, 2009, at 7:04 PM, Todd O'Bryan wrote:
>
>> or am I still not correctly verbalizing/understanding what I'm asking for?
>
> You are but like a typical consumer and many computer scientists, you are
> proposing a solution instead of stating and describing the problem.
>

That's largely because the problem reduces to, "I think there's
something wrong that could be improved and I have a vague sense of
what's wrong and what might fix it." Thanks for bearing with me.

> 1. We made the decision to go without static types for good reason. You
> don't want types (at the beginning).
I really do (maybe wrongly). Because if I don't have types at the
beginning, by the time types really count, students don't take them
seriously.

> 2. What we call contracts in BSL and what we call contracts in PLT Scheme is
> only loosely related. So you don't want contracts either.
Well, in the sense that contracts do dynamic type-checking, I think
Shriram's right and I do kind of want something like contracts within
modules.

> 3. In the German version of HtDP, dubbed DeinProgram, you state HtDP-style
> contracts in a formal language and they are checked as your BSL/ISL programs
> are run. It would cut down your students' 'debugging' time a lot. See
> DeinProgram in DrScheme, but you may need to know a bit of German.
>From what I can tell, these are a lot like the contracts module, but
they're executed on the current module rather than just across module
boundaries. Am I missing something or is that roughly correct?

I tried this program in Die Macht der Abstraktion - Anfänger

(: f (number number -> number))
(define f
  (lambda (x y)
    (+ x y)))

and it worked as expected. Keeping the contract, but changing the
function definition, I got:

(define f
  (lambda (x)
    x))

and an error:

1 contract violation.
wrong number of parameters, contract at line 1, column 5

Changing to put back the correct number of arguments, but mess up the
return type:

(define f
  (lambda (x y)
    "hi"))

This yields no error when you press Run, and you can even call

> (f 2 3)
"hi"

in the interactions window without an error.

If, however, you put (f 2 3) in the Definitions, you get an error:

1 contract violation.
got "hi" at line 6, column 0 , contract at line 1, column 23
to blame: procedure at line 3, column 2

This contrasts (obviously) with Typed Scheme, which throws a nice
error if you try

#lang typed-scheme
(: f : Number Number -> Number)
(define (f x y)
  "hi")

but Typed Scheme also checks the interactions, so if I type this
program in the definitions:

#lang typed-scheme
(: f : Number Number -> Number)
(define (f x y)
  (+ x y))

and then try, in the interactions window,

> (f 3 "7")
typecheck: Expected Number, but got String in: "7"

I get an error.

> 4. We intend to support something like this sooner or later. Robby has been
> working on this since 2004.
I'm happy to help with something like this. I think it would be worth
all the time I could throw at it. (It might not, however, be worth all
the time you might waste dealing with my stupid questions.

> 5. I don't understand how your students can have test cases for each
> function and NOT see that their functions are producing the wrong things.
> Code excerpts would be helpful.
Here's a common example with a single function:

;; A family-tree-node (ftn) is:
;; empty, or
;; (make-ftn ftn ftn symbol number symbol)
(define-struct ftn (father mother name dob eyes))

(define Carl (make-ftn empty empty 'Carl 1926 'green))
(define Bettina (make-ftn empty empty 'Bettina 1926 'green))
(define Adam (make-ftn Carl Bettina 'Adam 1950 'yellow))
(define Dave (make-ftn Carl Bettina 'Dave 1955 'black))
(define Eva (make-ftn Carl Bettina 'Eva 1965 'blue))
(define Fred (make-ftn empty empty 'Fred 1966 'pink))
(define Gustav (make-ftn Fred Eva 'Gustav 1988 'brown))


;; names: ftn -> list-of-string
;; consumes: a ftn
;; produces: a list of all names of people reachable
;;           from that ftn
(define (names a-ftn)
  (cond
    [(empty? a-ftn) ""]
    [(ftn? a-ftn) (append (names (ftn-father a-ftn))
                          (names (ftn-mother a-ftn))
                          (list (ftn-name a-ftn)))]))

(check-expect (names empty) "")
(check-expect (names Adam) (list "Carl" "Bettina" "Adam"))

The total error you get for this is:
append: expected argument of type <proper list>; given ""

Students look at the three arguments to append, see two calls to names
and a list. names's contract says it returns a list-of-string, so they
have no idea what could be going wrong. No, they don't notice the
inconsistency between the contract they wrote and the value of "" as
both the answer to one of the cond branches and one of their test
cases.

Where things really get confusing is if they use another function as
an auxiliary that they've written wrong tests for and the errors end
up buried inside the auxiliary call. As you said, checks within a
module would help *a lot* with this kind of debugging.

> P.S. For your reading pleasure, a first draft of the proposed teachpack for
> providing type-of and friends:
>
> #lang scheme
>
> (require lang/prim)
>
> (provide type-of)
>
> ;; Any -> Type
> (define (type-of a)
>  (cond
>    [(number? a) Number]
>    [(string? a) String]
>    [(boolean? a) Boolean]
>    [(procedure? a) Procedure]
>    [(type? a) Type]))
>
> (define-syntax-rule (def-types type? Name ...)
>  (begin (provide type? Name ...)
>         (define (type? x)
>           (member x (list Name ...)))
>         (define Name (gensym 'Name))
>         ...))
>
> (def-types type? Type Number String Boolean Procedure)

Thanks! I'll take a crack at this building on your starting point.
Please wait until I finish to tell me it's useless! :-)

Always appreciative of the fact that really great minds will take my
confused rants seriously,
Todd