[racket] Dynamic define-predicate

On Tue, Jul 6, 2010 at 7:00 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> 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)

This is a problem with using `define-predicate' in internal defintion
contexts, which is just a bug.

As to the larger issue ...

> 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.)

First, note that there's no way to infer what `a' should be in the
application of `id', so that will run into problems right away.

Second, I can't quite tell what you're trying to do.  Are you trying
to write a staged system, where the LC program *compiles* to Typed
Racket code?  Or are you trying to write a typed interpreter, eg
EOPL+Types?  Or are you trying to do the second thing, but with the
type-correctness of programs in the object language verified by the
meta-language typechecker?

If you're trying to do the third thing, which I think you are, I don't
think it will work in TR at all, and it's extremely unlikely to work
under this approach.  I don't see why you'd think that occurrence
typing would help you here.  Perhaps you can explain a bit more.

One place to look further is existing systems that encode the STLC in
the type system.  "The View from the Left", by Mcbride and Mckinna,
JFP 2004, has an example of this.
-- 
sam th
samth at ccs.neu.edu