[racket] typed scheme require question

From: Danny Yoo (dyoo at cs.wpi.edu)
Date: Tue Aug 17 13:03:49 EDT 2010

I'm using Racket 5.0.  I'm a little confused by the following.

I'm using typed/racket/base, and tried writing list-length using
'rest'.  rest isn't bound, so I did a typed/require to introduce the
'rest' binding.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#lang typed/racket/base

(require/typed racket/list
               [rest (All (A) ((Listof A) -> (Listof A)))])

(: list-length (All (A) ((Listof A) -> Integer)))
(define (list-length l)
  (cond
    [(null? l)
     0]
    [else
     (add1 (list-length (rest l)))]))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


This worked as expected.  I then wanted to see how the system responds
if I try using the untyped version; I wanted to see the kind of error
message I'd get back.  To my surprise, I didn't see any error when I
did the following:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#lang typed/racket/base
(require racket/list)

(: list-length (All (A) ((Listof A) -> Integer)))
(define (list-length l)
  (cond
    [(null? l)
     0]
    [else
     (add1 (list-length (rest l)))]))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


I'm guessing that the type-checker has some hardcoded notion of the
types for racket/list functions.  Is this true?


Posted on the users mailing list.