Add support for lambda abstraction

[ngeiswei]

Something that is still missing in MeTTa is a built-in support for lambda abstraction. Also, given that JeTTa apparently is going to support it, I think it's time we have a discussion about it to craft it exactly the way want while we can.

Here is my initial proposal

I suggest the following syntax

(\ PATTERN_1 ... PATTERN_N BODY)

where PATTERN_i is a pattern corresponding to the ith argument. Like in a regular MeTTa function, all patterns must unify with their respective arguments in order to beta-reduce.

For instance, the following call that takes the head of an empty list

((\ (Cons $head $tail) $head) Nil)

would not reduce, but

((\ (Cons $head $tail) $head) (Cons a Nil))

would.

Next, below is an example of a call with an n-ary function

((\ $x $y $z (+ $x (+ $y $z))) 1 2 3)

which would return [6].

The reason I suggest this syntax to define nary functions instead of say

(\ ($x $y $z) BODY)

is because, first, it is more consistent with the named function definition. For instance we say

(= (ternary-plus $x $y $z) BODY)

not

(= (ternary-plus ($x $y $z) BODY)

Although we can if we want to, we can do both!

And second, it is more consistent with type definition as well, for instance

(\ $x $y $z BODY)

corresponds to a type of tuple of the same size

(-> Number Number Number Number)

4 in both cases.

I believe that once lambda abstraction is natively supported, generic algorithms like map-atom and fold-atom should be upgraded to support it.

[vsbogd]

First option which comes to my mind is adding \ grounded operation which analyses the arguments and returns executable grounded atom which in turn can be called by interpreter.

[Necr0x0Der]

adding \ grounded operation which analyses the arguments and returns executable grounded atom

Yes, this is the simplest way. Maybe, we can implement it right away.
Meanwhile, we can analyze other options. What comes to my mind... Function are applied via equalities. Thus, either some equality should be added to some space, or application of lambda-expression itself should be carried out by a generic equality defined for lambda.
The former approach with adding an equality means that we have a grounded function \, which creates an symbol for the body and add the corresponding equality to the execution context space and returns the name of this function (e.g. (\ $x (* $x $x)) adds (= (f-0001 $x) (* $x $x)) and returns f-0001). I don't like turning anonymous lambdas into explicit functions too much, and we don't have such the temporary execution space. But there was such the space in the very initial implementation and design of MeTTa. And we may still want to introduce it back. It provides a lot of opportunities. But this is another story.

The latter approach is not impossible as well. The following code kinda works now even for arbitrary number of arguments (although values should be taken into parentheses):

(= ((\ $arg $body) $val)
   (let $arg $val $body))
!((\ $x (* $x $x)) 2) ; 4
!((\ ($x $y) (* $x $y)) (2 3)) ; 6
!((\ (Cons $head $tail) $head) (Cons a Nil)) ; a

I'm not sure, maybe, it can be improved with seal. Passing variables in metta may encounter some pitfalls. Maybe, we can start using this basic definition and see what the problems are. OTOH, if let is a grounded function, why couldn't we have \ to be grounded as well.... I'd prefer lambda-expressions to remain unreduced, though, until they are applied, so you can pass them back and forth, analyze them and modify...

[Necr0x0Der]

OK, well, I got the case, where it doesn't work.

(= ((\ $arg $body) $val)
   (let $arg $val $body))
(= (my-map $f Nil) Nil)
(= (my-map $f (Cons $x $xs))
   (Cons ($f $x) (my-map $f $xs)))
!(my-map (\ $x (* $x 2)) (Cons 1 (Cons 2 (Cons 3 Nil))))

It returns nothing. If we put (Cons ($f $x) (my-map-tmp $f $xs))) we see why. The output will be

(Cons 2 (my-map-tmp (\ 1 2) (Cons 2 (Cons 3 Nil))))

So, apparently, $x and $xs got substituted.

But with sealed it works!

(= ((\ $arg $body) $val)
   (sealed ($arg)
     (let $arg $val $body)))
(= (my-map $f Nil) Nil)
(= (my-map $f (Cons $x $xs))
   (Cons ($f $x) (my-map $f $xs)))
!(my-map (\ $x (* $x 2)) (Cons 1 (Cons 2 (Cons 3 Nil)))) ; (Cons 2 (Cons 4 (Cons 6 Nil)))

[Necr0x0Der]

I'm not sure that (sealed (($x $y)) ...) will work if we pass ($x $y) as variables. If it doesn't, we'll have to resort to something like:

(= ((\ $arg $body) $val)
   (sealed $arg
     (let $arg $val $body)))
!((\ ($x) (* $x $x)) (2)) ; 4

So, sealed $arg instead of sealed ($arg), but maybe we will need to always wrap even single variable and its value into parentheses. Not sure, more exploration might be needed.
Thus, if we want some syntactic sugar and want to support

(\ PATTERN_1 ... PATTERN_N BODY)

and if sealed doesn't work with variables in patterns, then maybe we should go for a grounded \. But if we are ok with parentheses and with extending sealed to extract variables from patterns rather than receiving them directly, then we might be able to save this approach. Once again, it's advantage is that expressions like (\ $x (* $x 2)) are pure metta expressions, which are not reduced by themselves and can be manipulated with.

[vsbogd]

I looked at the sealed code and actually it extracts all variables from the first argument thus it works with patterns as well. @ngeiswei you can try lambda implementation from #902 (comment) it should work as expected except one need use parenthesizes around patterns and arguments.

[ngeiswei]

That's a great suggestion, @Necr0x0Der, and is getting extremely closed to what I need. In fact one can overload \ to support the n-ary lambda abstraction I described, as showed below:

;; Nullary lambda abstraction                                                         
(: \ (-> Atom (-> $a)))                                                               
(= ((\ $body))                                                                        
   $body)                                                                             
                                                                                      
;; Unary lambda abstraction                                                           
(: \ (-> Atom Atom (-> $a $b)))                                                       
(= ((\ $arg $body) $val)                                                              
   (sealed $arg                                                                       
           (let $arg $val $body)))                                                    
                                                                                      
;; Binary lambda abstraction                                                          
(: \ (-> Atom Atom Atom (-> $a $b $c)))                                               
(= ((\ $arg1 $arg2 $body) $val1 $val2)                                                
   (sealed (, $arg1 $arg2)                                                            
           (let* (($arg1 $val1)                                                       
                  ($arg2 $val2))                                                      
             $body)))                                                                 
                                                                                      
;; Ternary lambda abstraction                                                         
(: \ (-> Atom Atom Atom Atom (-> $a $b $c $d)))                                       
(= ((\ $arg1 $arg2 $arg3 $body) $val1 $val2 $val3)                                    
   (sealed (, $arg1 $arg2 $arg3)                                                      
           (let* (($arg1 $val1)                                                       
                  ($arg2 $val2)                                                       
                  ($arg3 $val3))                                                      
             $body)))                                                                 
                                                                                      
;; Test nullary lambda                                                                
!((\ (+ 2 3)))                                                                        
                                                                                      
;; Test unary lambda                                                                  
!((\ $x (+ $x 1)) 2)                                                                  
                                                                                      
;; Test binary lambda                                                                 
!((\ $x $y (+ $x $y)) 2 3)                                                            
                                                                                      
;; Test ternary lambda                                                                
!((\ $x $y $z ($x $y $z)) + 2 3)                                                      
                                                                                      
;; Test unary lambda with pattern                                                     
!((\ (Plus $x $y) (+ $x $y)) (Plus 2 3))                                              
!((\ (, $x $y $z) ($x $y $z)) (, + 2 3))                                              

The only thing which is perhaps missing is local scope management, in the sense that a variable scoped under a lambda should be local and immune to collision with variables of the same name. For instance

;; Test nested lambda
!((\ $x (+ ((\ $y $y) $x) 1)) 41)

;; Test nested lambda with name collision
!((\ $x (+ ((\ $x $x) $x) 1)) 41)

;; Test nested lambda using sealed to avoid name collision
!((\ $x (+ ((sealed $x (\ $x $x)) $x) 1)) 41)

The last two nested lambda abstractions fail.

Another aspect of scoping is also to protect variables from unification. Indeed only free variables should be allowed to unify with terms different than themselves.