Just wanted to chime in and tell you a little about what I'm doing with the guile-unify package.
First off, this is a tool to do backtracking effectively e.g. tree searches and make heavy use of dynamic variables.
There is three activities ongoing.
1. type-checking examples 2. first order logic solvers (porting leanCop) 3. documentation
1. Documentation, I needed to recap somethings and started to improve on the examples above in order to achieve
higher generality. As it turned out bug's in the underlying code is squashed all the time and new useful features for the macro package is dicoverwed. So the codebase is in a pretty fluent state still. On the other hand some of the basic features
is being documented.
2. The core part of the first order logic leanCop solver has been translated to a macro package and are now in a pure scheme form. It's not that advanced. Then there is a language for how to state the problem especially a translational tool to gather information from a
database of first order logic problems. The idea now is to mod that tool into spitting out a file of of the translation which are working then call guile and let guile read in that file and process it with the core solver. The idea is to test out a few alternative solving teqniques
and evaluate their performance for the database.
3. For the type-checking examples I've been working with the assumptions of having fixed declarations for lambdas and deduce types for variables and their passage through the system. The thought is that in the end
one need to allow lambdas to be explicitly typed in order to allow advanced type-checking and at the same time avoid infinite recursions. I think that it's not uncommon in Haskell programming to add type information in order
to guide the type checker and being at such an infant stage having something useful and working must simple allow for type hint's in the code.
It would be cool to let emacs interact with guile to give a tool to automagically construct
type signatures aka (lambda (A) B) <enter> --> (lambda (integer) integer)
E.g. be able to interactively deduce a type signature.
I will try to add more type primitives like recursive types and so on to be able to match Haskel and typed racket.
Generally the biggest problem with backtracking is complexity issues. One can design relatively small programs that makes the type checker work for ages. i will not adress this right now but there are plenty of short cut's to be taken
in order to speed up the checker.
It would be good if there was a standard way to enter type information in guile and if that information could be hooked into the tree-il representation. But until then I will just use a simple macro framework to enter typed functions.
To note below if a lambda produces (or a b) then the rest of the code has to be tried with a and when checked then backtrack and be tried with b if both are type checked then we can proceed. (this is the naive and simple implementation) So we can have a general type checker but complexity wise
it will be awful. ------------------------------------------------------------------------------------------- So now this works in 1 sec, ********************** Code (have a geometric explosion in complexity e.g. works like 1000 lines of code) ******************
(tdefine (f X) (type (lambda (boolean) (or integer symbol)) ;; type signature is (type type-desc code ...) and gives a type hint to the lambda (let ((F (lambda (P) (type (lambda (boolean) (or integer symbol))
(if P 1 's))))) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #f)))) ************************************************** first stage compiled code ***********************************
(check (lambda ((#{X\ 10764}# : boolean)) : (or integer symbol) (begin (let #{F\ 10770}# (lambda ((#{P\ 10771}# : boolean)) :
(or integer symbol) (begin (if #{P\ 10771}# 1 (quote s)))) (begin (begin (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t))
(apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t))
(apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#f)))))))) ---------------------------------------------------------- **************************************** Deduced Equation *******************************
((= (lambda #<procedure 2a55800 at language/prolog/typecheck/equationalize.scm:72:2 ()>) Tres) ((= #{X\ 10764}# boolean) (= (lambda #<procedure 2a55760 at language/prolog/typecheck/equationalize.scm:72:2 ()>)
#{F\ 10770}#) ((= #{P\ 10771}# boolean) (or ((= (res #{P\ 10771}#) boolean) (= (res integer) (or integer symbol))) ((= (res #{P\ 10771}#) boolean) (= (res symbol) (or integer symbol)))))
(= (res #{F\ 10770}#) (lambda (arg Targ10777) Tres10778)) (= (res boolean) (arg Targ10777)) (= (res Tres10778) A10776) (= (res #{F\ 10770}#) (lambda (arg Targ10780) Tres10781)) (= (res boolean) (arg Targ10780))
(= (res Tres10781) A10779) (= (res #{F\ 10770}#) (lambda (arg Targ10783) Tres10784)) (= (res boolean) (arg Targ10783)) (= (res Tres10784) A10782) (= (res #{F\ 10770}#) (lambda (arg Targ10786) Tres10787))
(= (res boolean) (arg Targ10786)) (= (res Tres10787) A10785) (= (res #{F\ 10770}#) (lambda (arg Targ10789) Tres10790)) (= (res boolean) (arg Targ10789)) (= (res Tres10790) A10788) (= (res #{F\ 10770}#)
(lambda (arg Targ10792) Tres10793)) (= (res boolean) (arg Targ10792)) (= (res Tres10793) A10791) (= (res #{F\ 10770}#) (lambda (arg Targ10795) Tres10796)) (= (res boolean) (arg Targ10795))
(= (res Tres10796) A10794) (= (res #{F\ 10770}#) (lambda (arg Targ10798) Tres10799)) (= (res boolean) (arg Targ10798)) (= (res Tres10799) A10797) (= (res #{F\ 10770}#) (lambda (arg Targ10801) Tres10802))
(= (res boolean) (arg Targ10801)) (= (res Tres10802) A10800) (= (res #{F\ 10770}#) (lambda (arg Targ10803) Tres10804)) (= (res boolean) (arg Targ10803)) (= (res Tres10804) (or integer symbol))))
;;; compiled /home/stis/stis/src/guile/cache/guile/ccache/2.0-0.S-LE-8/home/stis/stis/src/guile/module/language/typed-guile/test.scm.go
************************************************************* Verdict defined f : (lambda (arg boolean) (or integer symbol))
$1 = #t