Transcript Java Mint: A Call for Questions

Java Mint:
A Call for Questions
Walid Taha
Rice University
Please open your mail client
and start writing
To: [email protected]
Subject: Your Java Mint Talk
... and send comments during the talk
Multi-stage Programming
In a nutshell:
• We love abstractions
• We don’t like to pay for them
• Multi-stage programming =
abstractions - runtime cost
Java Mint
Multi-stage programming worked nicely in
the purely functional setting
Can we do the same in bigger
languages?
This Talk
A call for discussion. The plan:
•
•
•
•
Defining “abstractions”
The functional theory of MSP (‘97-‘09)
Why this theory matters
Building the new theory
“Abstractions”
Abstraction Mechanisms
• A way of writing code so that is
– is parameterized, and
– can be instantiated by providing
parameters
• Note: no loss of information
We call them “abstractions” for short
Purely Functional Abstractions
•
•
•
•
•
Primitive functions
Lambda abstractions
Module definitions, and functors
Records
Variants (using “The Trick”)
MSP can guarantee the elimination of all of these
overheads
MSP types are well matched to a structural type system
Object-Oriented Abstractions
These are the kinds of things we would like to
deal with in the OO setting:
•
•
•
•
•
•
Objects (as records/fields)
Objects (as methods)
Object creation
Mixins (?)
Aspects (already staged?)
Design Patterns (?? Require formalization)
The Theory of Functional MSP
Why bother with “the theory”?
There is a huge body of results on various
technical aspects of functional MSP
What we don’t talk about much in
technical papers is how do we put all of
these results together?
We need to revisit this “big picture” at this
juncture
The Functional Theory of MSP
•
•
•
•
•
•
In (Static Types and Scoping) We Trust
Staging = modifying evaluation order
Future stage values are extensional
Staging annotations are lightweight (3+1)
Code type constructor is simple, orthogonal
Multi-stage Programming
– Naive: Just annotate
– Realistic: Convert to CPS, and annotate
The Functional Theory of MSP
• Staging affects only termination
• Programmers know how to ensure
correct termination behavior
• Statically typed program generation
= staging + expressive static types
• Expressive static types = CiC/Coq
What Does FMSP Matter?
• eval:
• seval:
exp * (id -> val)
exp * (id -> <val>)
-> val
-> <val>
• typecheck:
exp -> (!t . texp t) option
• teval:
texp t * (i:id -> T(i))
-> t
• steval: texp t * (i:id -> <T(i)) -> <t>
• bottom line: steval = 10 * seval = 40 * eval
Building the New Theory
Concrete Questions
• Can we achieve safe imperative MSP?
• Can we keep notation lightweight?
– Sam: Can we get away without HOFs?
• Killer app: FOP, Yannis’s examples?
• Can we avoid altering effects?
• Does Java need more expressive static types? If so, how can
we add them?
• Can we preserve extensionality?
• Can we improve break even points?
• Tim, Jacques: What will the PG programming style be, and how
do you teach it?
• Ras: Do programmers what to treat as early and what to treat
as late?
Bigger Questions
Can program generation gain broad, respectable
acceptance?
• Net Gain: Can we show that program generation
introduces less problems than it solves?
• Vanishing: Can we show that using program
generation is “just programming”?
• Doug: Certifying boards need to recognize things
other than testing for certification (such as program
generation). Can we generate certificates with
programs? (Is this already being done in the ORF
Tom Maibaum, FAA speaker at PCC)
Call To Action
Mint needs you!
• Designing a Meta-Java is harder
– Java is more complicated
– We want to take harder problems
• Need group involvement in
– Design, implementation, testing, evaluation
– Get on the list (tell me at top of your email)
Final Words
• OOMSP is an enormous challenge
• We should take on hard challenges
• We can meet hard challenges
– Coming up with environment classifiers
took 8 years
Acknowledgment
Thanks to the participants of the WG 2.11
for valuable discussions, and for
Jacques and William for feedback they
email after the talk.