Circular Instance Declarations

[Brandon Michael Moore]

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