Re: [boost] De Bruijn Bind (alternate bind syntax) Interest?

Subject: Re: [boost] De Bruijn Bind (alternate bind syntax) Interest?
From: David Sankel (camior_at_[hidden])
Date: 2010-09-02 13:33:18

2010/9/2 Stewart, Robert <Robert.Stewart_at_[hidden]>

> David Sankel wrote:
> >
> > I've been working on an alternate bind syntax based on De
> > Bruijn indices[1].
>
> I started to look at the Wikipedia page, but realized there was way too
> much for me to learn to even begin to understand what you mean.  Therefore,
> this reference is of no value to anyone without your background.
>

It requires someone casually familiar with lambda calculus. Lambda
calculus involves the creation of anonymous functions.

λv.e declares a new function. v is the identifier bound to the argument and
e is an expression that can use v. For example λx.x+1 creates a new function
that returns its argument plus 1. Expressions can include other lambdas
(called abstractions) and function applications.

Consider the function λx.λy.x+y. This function actually returns another
function which can be applied yet again. Here it is being called with some
values.

((λx.λy.x+y)(22))(14) ← here x is being substituted by 22
=>
(λy.22+y)(14) ← now y is being substituted by 14.
=>
22+14
=>
36

De Bruijn indices are a way to remove the need for binding a name to the
variable in our function declaration. So, instead of λv.e, where e can use
v, we say λe where e uses "1" to refer to the argument.

The reason for using 1 is to distinguish between between nested
lambdas. λx.λy.x(y) becomes λλ2(1). Note that 1 and 2 aren't the normal
arithmetic variants, these are De Bruijn indices. The 2 refers to the outer
lambda and the 1 refers to the inner lambda.

> Here is an example of a function const that takes in an argument c and
> > returns another function that, for all input, returns c:
> >
> >     //λx.λy.x = λλ1 with De Bruijn indices.
> >     auto const_ = abs<1>( abs<1>( var<1,0>() ) );
>
> Presumably, "abs" doesn't mean absolute value as it would in pretty much
> any other programming context.  That seems unwise at best.
>

I disagree. We have namespaces to take care of duplicate identifiers and abs
is the commonly used identifier for lambda abstractions in programming
contexts you might not be aware of.

> More examples, further explanation, and an implementation are
> > available here[2].
>
> I found your README.  The grammar section assumes I know what you mean by
> "abstraction" and "application," at the least, which I don't.  The examples
> section does absolutely nothing for me as I don't understand the syntax or
> terminology.  The result is that I can't make anything of your *bind*
> proposal.
>

Hopefully this helps. Thanks for the feedback.

David

-- 
David Sankel
Sankel Software
www.sankelsoftware.com
585 617 4748 (Office)