I'd like to use Typed Racket to create an interpreter for a typed lambda
calculus, which *inherits* Typed Racket's type system. (In other words,
I'm lazy and I don't want to make my own type system. But who does?
Except maybe Sam? :p) I was counting on occurrence typing to allow me to
do it while threading an Any-valued hash table environment, but I'm stuck.
Here's a snippet containing just the environment lookup function "id"
and relevant types:
#lang typed/racket
(define-type Env (HashTable Symbol Any))
(define: empty-env : Env (make-immutable-hash empty))
; type of environment idiom/monad computations:
(define-type (I a) (Env -> a))
(: id (All (a) (Symbol -> (I a))))
(define ((id name) env)
(define-predicate a? a)
(let ([val (hash-ref
env name
(lambda () (error 'id "not in scope: ~e" name)))])
(if (a? val)
val
(error 'id "runtime type error: unexpected value ~e" val))))
Running it gives:
Type Checker: Cannot apply expression of type False, since it is not a
function type in: (a? val)
I know the immediate trouble is with (define-predicate a? a). To behave
like I want it to, the type checker would have to look up or create the
predicate corresponding to the type of "a" at run time rather than
compile time.
Is there a deep/theoretical reason it can't work? Is there another way
to accomplish what I want that doesn't require passing a predicate to
"id"? (If I did that, I'd have to make the macro that expands to
expressions of type (I a) either keep track of types as it expands or
recursively transform ids in lambda bodies.)
Thanks!
Neil T
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
