LtU Forum

Sound and Complete Type Inference in BitC

Just a "head's up" that the extended version of the mentioned paper is now available on the BitC docs page. Given the amount of type algebra, it doesn't do very well in HTML. The PDF version is SRL2008-02. This is an extended version of our upcoming APLAS paper that includes all of the supporting proofs. So far as we know, this is the first sound and complete, integrative treatment of polymorphism and mutability in a single inference scheme.

Subsequent to this work, the BitC type system was revised to add a const meta-constructor and to re-specify mutability on a path-wise basis. This corrects a problem with deep immutability that was revealed by by-reference parameters and inner references. The revised type rules can be found in SRL2008-03. The revised rules remain sound and complete, and should be implemented in the compiler by some time early next week.

Still to come before we can release the first compiler are existential types, effect types, and structure subtyping.

I don't want to pick on Clojure (which looks very cool), but in light of the current discussion about state in Clojure, it may be appropriate to offer a counter-position:

Claim: If it isn't possible to efficiently self-host the runtime of your favorite functional language, then you can't argue credibly against imperative programming yet. At most, you might sustain an argument that imperative programming can (and perhaps should) be relegated to a very restricted part of your runtime library. This argument, in our view, evaporates in a puff of logic when performance criteria are admitted into the language evaluation.

In BitC, we take the position that pure programming is good when you can afford it (which is most places), but that there are places where we don't yet have any realistic alternative to imperative programming idioms.

ML Closure vs Scheme Closure

IIUC in ML lexical binding of variables leads to a copy of the variable, whereas in Scheme it is a binding to the variable memory location itself. Is there a common terminology to differentiate between the two different kinds of bindings? Am I understanding the difference correctly?

It also seems to me that the ML approach has a positive effect from a software engineering approach because it doesn't lead to a strong implicit coupling between modules. Has that idea been explored in the literature?

I am thinking of using ML style closures in my next language, what is the modern thinking on such an approach?

Can Lambda do things like arrays and matrixs? If so how?

Can Lambda do things like arrays and matrixs? If so how? (keep in mind im not good with math, and im not a programmer or anything, but i find concepts of math intresting)

Stock exchanges: language design aspect

This post is marginally on topic, touching social and economical sides of language design.

Recently I discovered to myself that orders for stock exchanges are little programs written in little language.
The concept of an exchange can be seen as an extension of the concept of money - while money relieves parties from necessity of finding right resources in right quantity to perform barter trade, exchange relieves parties from necessity of finding each other.
This is achieved by delegation of parties' decisions to smart (or not so) agents - usually called orders.

Orders historically started out as very simple agents - like "buy X units of Y for Z$". These agents would then be executed by exchange (in this simplest case, matching equal buys with sells).
With time, the DSL started to grow: "buy exactly X1 units of Y1 for up to Z$ by date D1 or else, buy up to X2 units of Y2 for the prevalent market price of date D2 but only if the prevalent market price of Y3 changed below Z3$ since the order was placed".

I found it very intriguing that exchange orders are not (usually publicly) presented as programs.
This may explain lack of attention from language design folks.
This again may explain why orders' DSLs are so ad hoc - though I certainly recognize there are a lot of other reasons, organizational and technical.
Another intriguing thing is that a lot of people placing their orders are not aware of exact rules for "order matching" (operational semantics of these DSLs). "It is performed by _the system_, why should I care about these details?"

Could it be that one venue to educate general public about languages and semantics is via articles about stock exchanges? :)

So the question: is anyone aware of any research for "better" orders language and/or "better" execution semantics for them ("better" being any of more intuitive/efficient/expressive/transparent)?

Scala programming job in Odersky's lab in Lausanne, Switzerland

Interesting Job notice on SEWORLD, the Software Engineering email list:

Excerpt:
This project aims at building an extensible workbench for automated program analyses of embedded software. The workbench will combine a number of static analyses and coordinate them using an evidence manager. Different program analyses will feed into each other. Their results will be presented to the software developer in a simple, uniform way, via a plugin for an IDE (Visual Studio). The plugin and the analyses will be written in Scala, and Scala is also the primary implementation language for which analyses should be constructed.

Project link:
TRESOR : EPFL Thrust in Reliable Software Research

(Disclaimer: I no connection with any of these groups, whatsoever. It just looked interesting.)

doing letrec with lambdas

Hi there,

I promise this isn't a homework assignment of some sort, but it sure feels like it should be....

I'm working on a pet language of mine, which I'm building up from a hopefully minimal intermediate language very similar to lambda-calculus. In order to map proper (potentially mutual) tail-recursion onto the lower-level implementation mechanics, I realized that I need to be able to do the moral equivalent of a letrec, but, since this's just a kernel-intermediate language, I want to avoid syntactic sugaring until higher-level intermediate forms instead, and would strongly prefer to not introduce a one-off level of complexity to hack this up. Doing "let" with lambdas is trivial enough that even I understand it, but I've gone 'round the proverbial mulberry bush with letrec, and to no avail.

Would someone either have a quick answer as to how this's done, or else know of a link to a site/paper/discussion where folks do this? This really can't be as hard as it seems....

Thanks!

Avoid -if- in the LOG function

Hello All:
I have written a log function to the project. Depending on the level in the log function(INFO) it displays the message. But in the log fn. i have a -if- which is called each time log is being called( like having an -if- for each printf of C). Is there a way to avoid the
-if- in the log function.
My Log call looks like:

LOG(INFO,"This Belongs to INFO Mode");
//INFO is of enum type

Suggestions are Acknowledged:
With Regards:

Review of a potential pramming language: Lima

Over the last 4 years I've compiled ideas about a programming language and have written a more or less extensive specification of the syntax. I was hoping some people here could review it for me. Link:

http://www.uweb.ucsb.edu/~frencheneesz/Lima/Frame_Lima_main.htm

I welcome any criticism, potential issues, or any other kind of discussion in general.

On a separate note, if anyone wants to help me develop the language, I would love the help.

Google chrome

Google releasing their own browser. This can be major news, with implications for various projects discussed here. There seems to be a boom in browser innovation recently.

They are apparently going to have their own Javascript VM (supposedly with JIT, and better GC). They implemented process isolation and sandboxing. This will clearly go in the direction of being a platform for application development (the relation to Android is intriguing). However, support for end-user client-side scripting (e.g., Greasemonkey) is not mentioned.

This is a developing story, as they say. I posted my thoughts about a google programming environment (and DSL) several times here. This may be a step in that direction.

What makes backreferences impossible in a DFA regular expressions evaluator?

Hello all,

I've been lurking for a while but this is my first post, so I apologize if I'm off-topic. I have read in papers such as this one that matching regular expressions with a "Thompson's NFA" or DFA makes matching backreferences inefficient (the above paper says it's np complete). Since I've written a regex engine that uses the "Thompson's NFA" algorithm as I understand it that matches backreferences efficiently in most cases, I'm assuming I am misunderstanding either Thompson's NFA or the use cases that can cause exponential runtime.

I've made the entire code available here, and I'm pasting the relevant code at the bottom of my post (it is short).

Why are backreferences considered impossible with a dfa regex engine?

BEGIN RELEVANT CODE

-- the compiler compiles a regex to a single MatchSequence
data RegexOp where
        MatchEndAnchor  :: RegexOp
        MatchChar       :: Char -> RegexOp
        MatchAny        :: RegexOp
        MatchSequence   :: [RegexOp] -> RegexOp
        MatchGreedy     :: Int -> Int -> RegexOp -> RegexOp -- min, max, operation
        MatchNonGreedy  :: Int -> Int -> RegexOp -> RegexOp
        MatchClass      :: [RegexOp] -> RegexOp -- used for character classes and (..|..)
        MatchLookAhead  :: RegexOp -> RegexOp
        MatchNegative   :: RegexOp -> RegexOp
        MatchBackRef    :: Int -> RegexOp
        BeginCapture    :: RegexOp
        EndCapture      :: RegexOp
    deriving (Eq, Show)

...

-- a possible state, our runtime keeps a list of all possible states by using the List Monad
data ReState = ReState {
    stream              :: String
    ,current_groups     :: [String]
    ,groups             :: [String]
    ,current_match      :: String
} deriving (Show, Eq)

...

-- start a new capture
--
push_capture :: ReState -> ReState
push_capture state = ReState (stream state) ([] : current_groups state) (groups state) (current_match state)

...

-- finish the newest capture and add it to our groups
--
pop_capture :: ReState -> ReState
pop_capture state = ReState (stream state) (tail $ current_groups state) (groups state ++ [head $ current_groups state]) (current_match state)

...

-- dfa_mkop is our main execution function, it takes an op and a state
-- and returns a list of all possible states
--
dfa_mkop :: RegexOp -> ReState -> [ReState]

...

dfa_mkop (MatchBackRef refnum) state =
        do
            g <- return $ groups state
            if length g < refnum
                then []
                else do
                    gval <- return $ g !! (refnum - 1)
                    st <- return $ stream state
                    if length st < length gval
                        then []
                        else if take (length gval) st == gval then [matched (length gval) state] else []

dfa_mkop BeginCapture state = [push_capture state]
dfa_mkop EndCapture state = [pop_capture state]

XML feed