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
