On Wed, 10 Sep 2003, Ashley Yakeley wrote:
Brandon Michael Moore <brandon@its.caltech.edu> wrote:
A simple irregular type is Irr a = Con a (Irr (F a)) (as long as F uses a)
Would this be an irregular type, with F as ((->) val)?
data SymbolExpression sym val a = ClosedSymbolExpression a | OpenSymbolExpression sym (SymbolExpression sym val (val -> a));
This would be an irregular type. In my proposal an instance declaration deriving some instance of SymbolExpression sym val a could use the types sym val and a in the context, but not (val -> a) which would only arise from unfolding the type constructor. Of course when I say "proposal" I mean "Would be a proposal if only I could prove that last lemma".
I used to use this in HScheme for expressions with free variables, as in the lambda calculus. For instance, "\x.xy" has "y" as a free variable, and might be represented as something like this:
OpenSymbolExpression "y" (ClosedSymbolExpression (\y -> (\x -> x y)))
It's very clean and safe, and can be made an instance of FunctorApplyReturn, but it turned out to be a bit slow. I also tried this:
data ListSymbolExpression sym val a = MkListSymbolExpression [sym] ([val] -> a);
MkListSymbolExpression ["y"] (\[y] -> (\x -> x y))
This is much simpler, but now one has to make sure that the lists are the same size, so to speak. But this one turned out to be the fastest:
newtype FuncSymbolExpression sym val a = MkFuncSymbolExpression ((sym -> val) -> a);
MkFuncSymbolExpression (\f -> (\x -> x (f "y")))
The downside is that there's no way to find out what the free variables are. That's OK for Scheme, however, since Scheme doesn't complain about unbound variables until run-time.
So, um, any excuse to talk about HScheme anyway.
It looks like your scheme puts the type system to good use. I used a value type with numbers, Val->Val functions, and some other stuff. I gave up when I realized I needed to thread references through everything to implement R5RS. I suppose everyone has started a Scheme in Haskell sometime. Brandon