[racket] Dynamic define-predicate

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

Shucks. (More on "shucks" below.)

> 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?

Ideally, I'd have a staged system using macros for the compiler, in 
which the type-correctness of programs in the object language (macro 
input) is verified by verifying expressions in the meta-language (macro 
output, or Typed Racket).

The code above is part of a compiler like this. In that one, Racket 
values directly represent object language values (e.g. object language 
integer = Racket integer), except for closures. So I had to compile to 
something that threads an environment. The reader monad / environment 
idiom is great for that.

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

Sure!

The *actual* thing I'm doing is a compiler in which object language 
expressions are represented by pure Racket accessor functions of a 
nondeterministic store. (It's like an alternative to the List monad.) 
You can mentally simplify it to a read-only store, which, though pretty 
useless, would interact the same way with Typed Racket. In any case, it 
all works great in untyped Racket.

In TR, the store has to have a type like (Listof Any) because statically 
discovering anything more specific is uncomputable. Object language 
expressions of type "a" are expanded to Typed Racket expressions of type 
((Listof Any) -> a).

It's not hard to make TR check object language expressions that don't 
read from the store. For example, in my current TR implementation, the 
expansion of (+ 3 'a) raises a type error. The error refers to functions 
a user would never see, but hey, it type checks. :)

What's hard is expanding expressions that *read from the store*. Suppose 
we're expanding (+ 3 x), and "x" represents a value of type Number in 
the store - which is of type (Listof Any). If TR didn't have occurrence 
typing, I couldn't construct a function of type ((Listof Any) -> Number) 
to represent "x".

But it does, and I can. The result looks very much like "id" above, but 
without the define-predicate. (The correct predicate is passed to the 
function that constructs it.) In general, I think you need either 
occurrence typing or dependent typing to pull this off. Very cool.

It has some limitations, though. 1) I have to track and pass around 
predicates that correspond with declared types. Not too big a deal. But 
I wouldn't have to do it if define-predicate worked in internal 
definition contexts on concrete types. 2) It only works for concrete 
types. This wouldn't exist as a limitation if define-predicate worked on 
type variables.

I think there are ways to make define-predicate work on type variables. 
The implementations I can think of (with my limited understanding of TR, 
mind) require making an instance of a function per instance of a type 
variable, invisibly passing types to functions, or having functions 
discover which site they were called from. They are all very icky.

But it's not critical. I knew it would be hard to transform my object 
language into a typed language and get some type checking for free. I 
just wanted to see exactly why.

Neil T