Polymorphic function `car' could not be applied to arguments

Question

I want to use typed/racket to implement the "LET" language in eopl, but I encounter problems： I try to implement three functions( empty-env, extend-env, apply-env ), but I don't know how to label the type information, and racket cannot automatically deduce the types of these three functions. I tried to use any, but I still encountered problems：

(: empty-env (-> Any))
(define empty-env
  (lambda () (list 'empty-env)))

(: extend-env (-> Any Any Any Any))
(define extend-env
  (lambda (var val env)
    (list 'extend-env var val env)))

(: apply-env (-> Any Any Any))
(define apply-env
  (lambda (env search-var)
    (cond [(eqv? (car env) 'empty-env) (None)]
          [(eqv? (car env) 'extend-env)
           (let ([saved-var (cadr env)]
                 [saved-val (caddr env)]
                 [saved-env (cadddr env)])
             (if (eqv? search-var saved-var)
                 saved-val
                 (apply-env saved-env search-var)))]
          [else (None)])))

The error prompted by racket is：

Type Checker: Polymorphic function `car' could not be applied to arguments: Domains: (Listof a) (Pairof a b) Arguments: Any in: (car env)

How can I correctly label the type information

Answer 1

I've found that having a list of arbitrary length of mixed types doesn't really play well with typed Racket (True, but not relevant to OP's original code; I was looking at an earlier version of mine when I said that), and that Any should be used sparingly (If you're using it for all types, might as well use normal Racket, for one). Using a list of pairs for your environment (Or better yet a list of structs, but I'm not familiar with EOPL and what it covers) is the way to go here. Something like:

#lang typed/racket

;; Type that associates a symbol with an arbitrary value                                                                                                                                                                                         
(define-type Binding (Pair Symbol Any))
;; A list of these is your environment/symbol table.                                                                                                                                                                                             
(define-type Env (Listof Binding))

(: empty-env (-> Env))
(define empty-env
  (lambda () '()))

(: extend-env (-> Symbol Any Env Env))
(define extend-env
  (lambda (var val env)
    (cons (cons var val) env)))

;; made up so the below will compile                                                                                                                                                                                                             
(define None (lambda () 'None))

(: apply-env (-> Env Symbol Any))
(define apply-env
  (lambda (env search-var)
    (if (null? env)
        (None)
        (let ([saved-var (caar env)]
              [saved-val (cdar env)])
          (if (eqv? search-var saved-var)
              saved-val
              (apply-env (cdr env) search-var))))))

Answer 2

#lang typed/racket

(define-type EmptyEnv '(empty-env))
(define-type Env      (U EmptyEnv
                         (List 'extend-env Any Any Env)))

(define (None) 'None)

(: empty-env (-> Env))
(define empty-env
  (lambda () (list 'empty-env)))

(: extend-env (-> Any Any Env Env))
(define extend-env
  (lambda (var val env)
    (list 'extend-env var val env)))

(: apply-env (-> Env Any Any))
(define apply-env
  (lambda (env search-var)
    (cond [(eqv? (car env) 'empty-env) (None)]
          [(eqv? (car env) 'extend-env)
           (let ([saved-var (cadr env)]
                 [saved-val (caddr env)]
                 [saved-env (cadddr env)])
             (if (eqv? search-var saved-var)
                 saved-val
                 (apply-env saved-env search-var)))]
          [else (None)])))

(define env (extend-env 'a 42 (empty-env)))
env
(apply-env env 'a)