FWIW, I agree with Robby and have had similar conversations with Sam
in person. (Although for me it is that I wish I had the ability to
claim that macro pieces had certain types regardless of what TR could
infer from the generated code.)
I think a big part of the Racket philosophy is that the programming
language implementer is not a member of an elite, enlightened caste
that can make choices mere mortals cannot. This philosophy is the root
of what I find beautiful about macros, continuations, first-class
synchronization, and structure type properties, for example.
Although I am not directly writing anything for the TR implementation,
I have opinions about the goal of that project. To me, it is not
figure out a type system that is passable for Racket programs but
make a type system that is to existing type systems as Racket is to
pedestrian languages in particularly, by allowing more
extensions (type or otherwise) to be done in language.
I see Robby's point about contract / type isomorphism and mine about
more powerful type macros as steps in that direction.
3
Jay
On Tue, Jun 26, 2012 at 10:10 PM, Robby Findler
ro...@eecs.northwestern.edu wrote:
Consider me done!
Robby
On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto neil.toro...@gmail.com wrote:
I haven't got a clue what you two are arguing about anymore. If you both
stop, maybe Sam can implement that perfectly safe change to the typed -
untyped contract barrier that he said he could do. That would be nice.
;)
Neil ⊥
On 06/26/2012 09:23 PM, Robby Findler wrote:
On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadtsa...@ccs.neu.edu
wrote:
On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler
ro...@eecs.northwestern.edu wrote:
On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadtsa...@ccs.neu.edu
wrote:
On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler
ro...@eecs.northwestern.edu wrote:
This sounds like a terrible solution.
There are lots of places in our system where we just declare facts and
don't prove them and then use them for lots of things (often
optimizations). Why should this one be special?
I don't know of any places like this in Racket. What are you thinking
of?
The inliner and the JIT compiler and that whole interaction are the
ones I thought of. I should have said lots of facts not lots of
places, tho. Sorry about that.
I'm still not sure what you're thinking of. What operation does the
inliner or JIT perform that is justified by a
programmer-declared-but-not-checked fact?
There are many operations that are implemented partially in JIT and
wholly in the runtime system. The JIT generated version gets used
unless certain conditions hold, in which case the runtime system
version gets used. The programmer declared fact is embedded into the
code and not specified as a fact per se, but for example, there is one
such fact saying this pile of assembly instructions is equivalent to
the C implementation of list-ref, under the condition that the number
argument is a fixnum less than 10,000 and we don't run out of pairs
too soon (roughly). There are large pile of such things. Another one
you're probably more familiar with: this pile of assembly
instructions is equivalent to + when the arguments are both fixnums or
both flonums.
There is another pile of such invariants in the (pre-bytecode level)
inliner. It relies on beta substitution and the ability to run certain
primitives at compile time. (I don't know as much about that one, so
probably there are more things it relies on than that.)
Certainly, Typed Racket is intended to be sound in the same sense that
Racket is safe, and that Haskell, OCaml, and Java are safe as well: if
you don't use specifically-marked unsafe features (such as the FFI and
`racket/unsafe/ops`), then you get a guarantee that depends only on
the correctness of the runtime system/compiler, not on the correctness
of any user code.
Of course I understand this. I'm pointing out that this is not a
significant guarantee, in and of itself (see last para below for an
elaboration here).
I think this a very important guarantee: we've seen
far too often that trusting user code in languages like C and C++ was
a big mistake in many contexts.
I don't think this is an either/or. Indeed, just to continue with C:
if everyone understood that the types were really just size markers
and nothing else, then lots of the seeming unsoundness goes away in C
(not all, of course, and as I've been learning from Regehr's blog,
there are lots of other dark corners). But no one is suggesting we
remove checks from array bounds, which is what really cost society
money wrt to C and, IMO, the kind of invariant that matters.
I don't think the distinction that you're trying to draw here is
meaningful. In particular, to return to our earlier example, if you
assert the type Neil gave for an untyped value, backed up with the
contract `(- real? real?)`, then Typed
