On 08/08/2012, at 9:31 AM, Dobes Vandermeer wrote:
> On Tue, Aug 7, 2012 at 4:18 PM, john skaller <skal...@users.sourceforge.net>
> wrote:
>
> On 08/08/2012, at 8:15 AM, john skaller wrote:
>
> > I have confirmed there is a bug in the recursion detection algorithm.
> > Well actually not a bug so much as a design fault.
>
>
> BTW: there's another bug in the same algorithm: it doesn't detect
> unused children correctly. When I set Sexpr's str function to inline,
> stuff no longer blows up, but some used children get deleted
> leading to subsequent error where an reference to one of them
> is reported not found.
>
> Maybe you can file all this stuff in github for posterity?
That would require writing it up twice :)
There are lots of things that need reworking, as well as new things to add.
Too many to write up unless that would lead to resolution.
It would be cool is some academics would put some students onto
some of these tasks. Here's an interesting one:
In type classes we have default implementations, for example we might
write:
class Equal[T] {
virtual fun == (x:T, y:T) => eq (x,y);
virtual fun eq (x:T, y:T) => x == y;
}
As long as you instantiate one of these everything is fine. If you forget,
you get infinite recursion. More generally, the question arises:
"Does the set of functions of an instance of a class for a basis for the set of
virtuals? Or some subset of them? Is the set overspecified? If so, is the
set consistent?"
In the Equal example above, an implementation of one or the other
of the functions forms a basis. If neither are implemented the class is
underspecified, if both overspecified.
In general a class is "safe" if the virtuals form a basis (without defaults),
and it is easy to see the rule then is that you must specify exactly all the
virtuals -- no less (you can't call a pure virtual) and no more (well,
there aren't any more).
In a more general case, the dependencies can be established from the
axioms. Default values of virtuals are reducible axioms. Correctness, however
requires a proof. In simple cases correctness can be established by
an automatic theorem prover. This has been done previously in Felix
using Why2 interface and Ergot prover (both written in Ocaml). I have also
managed to get Simplify to work.
In cases where an automatic prover cannot cope, we would like to provide
instead a proof sketch such that the prover can now be guided by the sketch
and complete a proof. Of course in even more difficult cases we may have to
use an interactive proof assistant like Coq.
Felix already has a notation for this: lemmas are propositions which can be
proven automatically by current provers. Theorems are propositions
which would require a proof sketch (but there's no notation for such
sketches).
However, whilst proof of correctness is an ideal, at least establishing
dependencies
in some cases would be useful: it might help stop the infinite recursion
in Equal if we forgot to provide at least one instance.
Note that Haskell cannot do this either! Nor can C++ or other OO languages
where exactly the same problem arises.
in general we do NOT want to provide a fixed basis as virtuals.
This is a bad idea because it is inefficient and it may force an uncomfortable
choice on the programmer. Just to illustrate, here's another example:
class TotalOrder [T] { == != < <= > >= }
I didn't bother to define the comparisons because I'm sure readers get the
picture.
You can actually do a total order with ONLY operator < plus the usual features
of applicative programming eg:
fun > (x,y) = y < x;
Here we have an even worse problem. Its not just a matter of defining defaults
for all the operators, so you could define > instead of <, or <=, but not
merely ==,
no, here its worse: there are MANY possible defaults for each function,
depending
on which other operators are defined.
Some of these might be derived from a single default plus axioms.
You can see this is getting really messy now! The core problem here is that
picking a fixed basis, or maybe having just two, whilst common in mathematics,
is entirely inappropriate in a programming language. Your virtuals should be
a set of properties beyond a basis, for ease of definition and performance.
Your "axioms" will be over specifications.
Felix does not need a solution to this: Haskell doesn't have one.
Its just a risk, if you do things wrong, all hell breaks loose and you got no
warning from the compiler. Hard to debug. But some work in this area might
lead to earlier diagnosis.
OK, so I'm just mentioning this one little issue where work could be done
to improve the system. There are THOUSANDS of such topics, enough
for hundreds of PhDs.
There's little point writing up some nice cases like the above example
without a supply of people to work on them. I can work on them and
at this stage I'm the supply and if I wrote up all the cases I'd never get
to address any of them.
Some of these issues, like the one above, are well "encapsulated"
in the sense that they're easily specified and require work in a very
isolated and separable part of the compiler. There are many of these too.
Just pick an area you want to work in and I'll find you a problem to solve :)
Here's another nice one: split out the parser completely from Felix.
Remove all dependencies so it can act as a completely separate
stand alone GLR parser (with dynamic loading from EBNF).
Dypgen can do this in its base form, but that requires compiling Ocaml
and linking it to your project. With a stand alone parser we can
print out the syntax tree (as XML or S-expressions for example).
Another parser job: figure out how to make the parser able to call
itself recursively. What we want to do is this:
expr := expr ">>=" expr => bind ($1, $2)
That is, we want to write Felix (with "holes in it") as the action code for
the production instead of writing Scheme, which is what you have to
do now.*** In theory this isn't hard. In reality I can't see a way to do it
because Dygen can't be invoked recursively.
*** the result of the RHS would be a Scheme function which accepts the $1 and $2
arguments and generates an s-expression.
--
john skaller
skal...@users.sourceforge.net
http://felix-lang.org
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
