Friday, December 26, 2008

Making stuff

So we're ripping out the parser again next time — by "we're" I of course mean "I'm" — and since we really want and/or need strong typing, I'm writing a type-inference engine. Yay! (I did write a compiler in college, but that was for Pascal, which doesn't have anything like type-inference: programs are explicitly typed, and either are correctly typed or not. So I'm enjoying this.)

It's a parser for mathematical expressions, rather than for one of our data formats; since I'm rewriting it, I'm also normalizing and extending the expression language. The old expressions were strictly arithmetical, but I chafe at this and wish to write custom functions. Therefore, the new expressions will basically be the simply-typed lambda calculus, extended slightly — both parametric and ad-hoc polymorphism (the latter technically only for built-in operators). From my limited understanding, it's not quite System F, as it's still amenable to Hindley-Milner type-inference, or something sufficiently like it. I'm also going to be flirting with one of the other axes of the lambda cube, since the language will hopefully eventually include fixed-size collections — array [8] of int and the like. Since I want let-expressions and, eventually, fixed-size collections, I'll probably use a more general constraint-solving approach (assuming I understand that paper correctly).

I've been debating adding a cons operator (a → [a] → [a]), since it looks like I'm going to have to deal with GC anyway. (Since there are neither cycles nor a fixpoint operator, ref-counting should suffice. I think.) Lists being an inherently recursive species, it's not very useful without recursion, mind; but foldr and iota :: Integer → [Integer] as "primitives" (and probably map, too, even though map f xs = foldr (cons . f) [] xs) should keep recursions out of the type-inferrer and guarantee termination.


Edited 2008-12-27: Except, really, we don't need it, so I won't. We'll have something like type-inference, but there will be no lambdas, nor higher-order functions.

No comments: