Re: [Axiom-developer] Re: Lisp may not be dead, but...

[Peter Broadbery]

On Thu, 2006-05-25 at 21:05 +0200, Martin Rubey wrote:
> Dear Peter,
> 
> Peter Broadbery <address@hidden> writes:
> 
> > > (did you send this in private intentionally?)
> 
> > Feel free to forward.
> 
> done
> 
> > > Peter Broadbery <address@hidden> writes:
> > > 
> > > > Forcing the interpreter to understand dependent types is a bit of an
> > > > unknown quantity to me - my sole attempt at trying ended up with the
> > > > aldor compiler crashing while creating the .asy file, so I couldn't see
> > > > what axiom would do with it.  Having the aldor source would have been
> > > > nice at that point.  My suspicion is that it would be possible to fix 
> > > > the
> > > > interpreter, at least as far as function lookup.
>  
> > > > Types as 100% first class objects might be difficult in axiom as is -
> > > > there's a lot of stuff in function lookup that works from the name of a
> > > > type as opposed to a value.
> > > 
> > > Well, one thing we currently need for Axiom-Combinat is to be able to have
> > > a List of domains, and be able to pick one and use it. I'm afraid that's
> > > about as far as first class can get... Still, we really need that.
> > > 
> > Do these domains have a common category?  
> 
> Yes.
> 
> > Do you need the precise exports of the domain, or is the category enough? 
> 
> I'd guess that the category is enough. Not sure here. But any progress would 
> be
> great, of course.
> 
> > Boxing the domains within a common one for axiom's purposes might be 
> > possible
> > - or you've tried that one?
> 
> Not sure what you mean here.
> 

[This may be a bit revolting] Let's suppose that these domains are all
in the category X, exporting f: () -> %.  NB: Untested.


XisADomain: with {
        aDomain(T: X): %;
        f: () -> XD;
} == add {
        Rep ==> X;
        aDomain(T: X): % == per T;
        f(): XD == makeXD(X, f()$T);
        -- and similar for any other nullary exports of X.
}

XD: X with {
        makeXD: (T: X, a: Pointer) -> %;
} == add {
        Rep ==> Record(T: X, a: T);
        makeXD(T: X, a: Pointer): % == per [T, a pretend T];

        -- need to implement all the operations of X here, example:
        g(o: %): % == {
                (T: X, a:T) := per o;
                per [T, g(a)$T];
        }
}

Any functions returning a list of domains should have [aDomain(T) for T
in L] run across them before axiom sees them.  makeXD has the wrong type
- it should be makeXD: (T: X, a: T) -> %, but see comments about .asy
files.  

> > As far as me trying to update axiom - I never had a great deal of exposure 
> > to
> > how the type handling worked in axiom - that said, if there is an obvious 
> > way
> > of making dependent types work (and even 1st class domains), I'd be willing
> > to have a stab at it, time permitting.
> 
> PLEASE do. It seems that you are the only one with the knowledge who is still
> around!
> 



> 
> Thanks, for everything,
> 
> Martin
-- 
Peter Broadbery <address@hidden>