[<<][staapl][>>][..]Thu Jul 17 13:25:40 CEST 2008

Jan 22 2007 @ google: http://video.google.com/videoplay?docid=915594482273345538&q=type%3Agoogle+engEDU Research question: What are the high level abstractions that can be used to keep control over resource use? goal: - support expressive abstractions - ensure safety by static analysis - don't let this get in the way means: - multi-stage programming (MSP) - reactivity (I/O events) - advanced type systems ( Staapl does MSP in a traditional untyped / partly dynamically typed way, without special tools for reactivity and static type analysis. Contrasting principle: get MSP to work first in a simple paradigm, add static tools later using DSLs. ) Ideas behind MSP are old. The new approach is to combine this with static tools. Reactivity is combined with MSP by creating program generators for reactive programs with static guarantees. Essence behind typed MSP: extend with types that are - delayed value - annotated what kind of delayed value ( An essential concern that seems to be solved by MetaOcaml is variable capture. The lucky thing about Staapl is that this problem is avoided: there is never any confusion about binding of values: in the pattern definition language standard Scheme lexical binding is used, while in composition, there are no bound names: all is point-free. The big disadvantage of course is that a stack language has no parameters. For multi->multi DSP code this is a problem. However, FP like array processing languages can be embedded in a similiar point-free style, replacing the stack with array structures that also can be re-used in every step. The essential insight is that it's not stack computing that's important, but point-free threaded state that gets discarded after each function application. ) What pops out of the FFT example in the talk is the use of mathematical properties in the generation of the code: algebra of programs, where the program in this case is ordinary algebra :) Reactive programming: E-FRP, a scaled down version of FRP from Haskell which compiles to event-loop C-code. Linear types: values can be used only once (consumed). Hoffmann (LFPL). The idea is that in pattern matching, on deconstructs a cons cell, which is then passed to the RHS where it can be reused: cons(x, xs) at d -> cons(1, xs) at d Indexed types: a bit like polymorphic types, but with parameters that have values, i.e. lists of a certain size. This goes pretty far: you provide proofs that the type checker checks. This can be very specific: nasicly, the types could be made to perform the whole computation completely in the type system. EDIT: look at dependent types, Pierce p. 462 Onwards, maybe this is interesting: gradual typing: http://lambda-the-ultimate.org/node/1707 ( About domain specific knowledge and rewrites: basicly, these are theorems about the data types and operators. This might be abstracted by generating parameterized theorems, but then those can probably be specofied as more complicated rewrite rules. One possible step is to start from equations, and distill directed rewrite rules. )

[Reply][About]

[<<][staapl][>>][..]