Some guile-unify activities

[Stefan Israelsson Tampe <stefan.itampe@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 6835 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 7403 bytes --]