Cool!
On Fri, May 6, 2011 at 5:18 PM, Stefan Israelsson Tampe
<stefan.ita...@gmail.com> wrote:
> Hi,
>
> 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
>
> /Stefan
>