Some guile-unify activities

Some guile-unify activities

[Stefan Israelsson Tampe]

[-- 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 --]

Re: Some guile-unify activities

[Noah Lavine]

Cool!

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

Re: Some guile-unify activities

[Ludovic Courtès]

Hey,

Nice stuff!

Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> 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.

FWIW the Hindley-Milner type inference example of Mini-Kanren works
well, at least for simple cases:

--8<---------------cut here---------------start------------->8---
scheme@(guile-user)> (run* (q) (!- (parse '(lambda (x) (+ x 1))) q))
$1 = ((int -> . int))
scheme@(guile-user)> (run* (q) (!- (parse '(lambda (x) (zero? x))) q))
$3 = ((int -> . bool))
--8<---------------cut here---------------end--------------->8---

Thanks,
Ludo’.

Re: Some guile-unify activities

[Andy Wingo]

Hi Stefan,

Thanks for this mail, it's interesting.

On Fri 06 May 2011 23:18, Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> 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.

Agreed, that this would be good.  Something to think about for 2.2.

Happy hacking,

Andy
-- 
http://wingolog.org/

Re: Some guile-unify activities

[Stefan Israelsson Tampe]

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

Hmm, type annotations in typed racket is defined according to

http://docs.racket-lang.org/ts-guide/more.html#%28part._.Type_.Annotation_and_.Binding_.Forms%29

Any objections against that scheme? ideas?

A suggestion would be to have a type item in tree-il that works like
(<type> type expression)

And at first stage let tree-il->glil code just ignore this information.

For <let>  tree-il code  we could just use the method
(let ((x : number 1)) code)
-->
(<let> ((<type> number x)) (1) code)

For lambda expressions we could use
(lambda ([x : integer]) : symbol code)

as

(<lambda> ((<type> integer x)) (<type> symbol code))

So, a first step would be to enter a type tree-il record and then make sure
that various tree-il->* translators can
use them (ignoring them at first). modify scheme->tree-il  to allow typeed
variants, and also enter a (type x) form
directly.

What do you think?


On Sun, May 8, 2011 at 5:52 PM, Andy Wingo <wingo@pobox.com> wrote:

> Hi Stefan,
>
> Thanks for this mail, it's interesting.
>
> On Fri 06 May 2011 23:18, Stefan Israelsson Tampe <stefan.itampe@gmail.com>
> writes:
>
> > 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.
>
> Agreed, that this would be good.  Something to think about for 2.2.
>
> Happy hacking,
>
> Andy
> --
> http://wingolog.org/
>

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

Re: Some guile-unify activities

[Andy Wingo]

On Mon 09 May 2011 13:15, Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> Hmm, type annotations in typed racket is defined according to
>
> http://docs.racket-lang.org/ts-guide/more.html#%28part._.Type_.Annotation_and_.Binding_.Forms%29
>
> Any objections against that scheme? ideas?

I think that what I'm primarily interested in is a way to annotate
tree-il with type information, which the compiler may use to generate
more efficient code.  However I think it's premature to bless a
particular encoding of that information in Scheme, or any particular
type system... basically it should be a field in the tree-il, I think,
and anything else can be built on top of that.

MHO anyway :)  But yes, there is a lot to learn from Racket about this.
They've done the most advanced work that I'm aware of.

Andy
-- 
http://wingolog.org/

Re: Some guile-unify activities

[Stefan Israelsson Tampe]

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

I looked in psyntax.scm, I should be able to add some extra fields to the
tree-il representation as you wish.
I will have a try of it


>I think that what I'm primarily interested in is a way to annotate

> tree-il with type information, which the compiler may use to generate
> more efficient code.  However I think it's premature to bless a
> particular encoding of that information in Scheme, or any particular
> type system... basically it should be a field in the tree-il, I think,
> and anything else can be built on top of that.
>
> MHO anyway :)  But yes, there is a lot to learn from Racket about this.
> They've done the most advanced work that I'm aware of.
>
> Andy
> --
> http://wingolog.org/
>

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

Re: Some guile-unify activities

[Andy Wingo]

On Mon 09 May 2011 20:35, Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> I looked in psyntax.scm, I should be able to add some extra fields to
> the tree-il representation as you wish.  I will have a try of it

Just to warn you that I'm fairly opinionated about these things; your
patch may or may not make it in.  You will also need to change
tree-il.scm, expand.[ch], and possibly memoize.[ch].

But good luck!

Andy
-- 
http://wingolog.org/

Re: Some guile-unify activities

[Stefan Israelsson Tampe]

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

wingo wrote:
> Just to warn you that I'm fairly opinionated about these things; your
>
patch may or may not make it in.  You will also need to change
>

It's better to code and loose then never code at all
jokes aside, I'll will take this in small smelling shebackas. Main point is
not me
coding, the main point is to get this question moving :-)


tree-il.scm, expand.[ch], and possibly memoize.[ch].
>

Good hint's here, thanks!

/Stefan

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

Re: Some guile-unify activities

[Andy Wingo]

On Tue 10 May 2011 11:00, Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> It's better to code and loose then never code at all

Yes!

> jokes aside, I'll will take this in small smelling shebackas. Main point is not me
> coding, the main point is to get this question moving :-)

Cool.  Happy hacking!

A
-- 
http://wingolog.org/