Re: Some guile-unify activities

[Noah Lavine]

Cool!

On Fri, May 6, 2011 at 5:18 PM, Stefan Israelsson Tampe
<address@hidden> 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
>