Sam Tobin-Hochstadt wrote:
On Tue, Jul 6, 2010 at 7:00 PM, Neil Toronto <neil.toro...@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
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
