Re: The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

Hi Noah,

On Wednesday, November 24, 2010 02:54:37 am Noah Lavine wrote:
> Hello,
> 
> That might make sense. The documentation certainly looks interesting.
> 
> What I'm thinking of is like racket contracts, but with the idea of
> "trusted modules", which might involve static checking. For instance,
> if the contract is that map's second parameter is a list, you'd
> normally want to check that. But if a module that used map could
> guarantee that it would always pass a list as the second argument,
> then you'd arrange things so the second module could skip the type
> check.

Sure static typechecking can save some time, but also note that it can bring
in applications that would not be on a scheme platform without static 
typechecking/proofing due to code safety reason imaginable or not 
(again static versus dynamic). An intersting note, one here stories about 
codebases around a popular dynamically p.l. where the test harness grow out 
of bounds and where the major part of it is test that the static typechecker 
would have been performed by default in both a much faster manner and also
more rigourusly. Personally I prefere dynamic - but that is from my usage 
pattern which is mainly smaller programs that automate. Form this I'm 
wondering if the people in this hersay really take advantage 
of testing only the relevant parts of the code in light of done changes. 

> I'm curious in general though whether it would be possible and
> worthwhile to statically check programmer-defined ideas, as long as
> the interface is easy enough to use. For instance, what if you could
> ask Guile to check that your tree structure always remained a binary
> tree? Or better, what if you wrote a GUI program and checked that the
> callbacks you passed to the GUI library would always return? (I know
> it's not possible in general, but I think it will work for a subset of
> procedures that will include some interesting ones.)

Yep I agree with you here.

Here is an idea:
You can try to say something like this function argument will never be 
returned or kept in a closure etc. Then you might allocate that object from
the stack. Again it is not always ways to proove this but sometimes you
can. So the function argument could be of a proved not proved and don't know
and you can make sure to use the safe way. Then you can guide a user to prove
that it is indeed so or let the user say it is so or just take the safe path 
and allocate from the heap. There is a nice pattern here that one could employ
when there is a compiler for guile (without compiler the speedup is not that
exiting on a relative scale). Process the code and builed up the result using
a tail call paraadigm, e.g. there is a parameter res that is constructed. Then 
at the end return (heapify (revers ret)) and transfere the constructed ret 
object to the heap by trying to fill a continuous segment on the heap by cons 
cells that is linked appropriated. That way you get some work to align objects
on the heap, allocate a big chunk at the time and the overall performance
scale and is performat. I would say that 99% of the code I write that use or
could use this pattern can be typechecked to proove that res could be builed
up from stack elements. The typical usage scenario here is to speed up 
functional (no mutating) code transformations. 

Have fun
Stefan