Re: [stack] Re: Some thoughts on Object Cat

On 20/4/08 2:12 PM, "Christopher Diggins" <[email protected]> wrote:

>  
>  
> 
> On Sat, Apr 19, 2008 at 11:56 PM, John Nowak <[email protected]
> <mailto:john%40johnnowak.com> > wrote:
>> >
>> >
>> > On Apr 19, 2008, at 10:58 AM, Christopher Diggins wrote:
>> >
>>> > > One paper caught my eye
>>> > > "http://research.microsoft.com/users/daan/download/papers/hmf-tr.pdf"
>>> > > which talks about impredicative instantiation. This is interesting
>>> > > because it is precisely the problem we talked about previously, and
>>> > > that Colin Hirsch pointed out to me even earlier. I didn't realize
>>> > > that the solution was not so well known. I actually do not use the HM
>>> > > type inference algorithm.
>> >
>> > (I assume the problem you're talking about is writing things like the
>> > 'm' combinator.)
> 
> No, I was referring to the "ambiguous impredicativity" problem of
> dealing with polymorphism that he refers to. It seems that nested
> polymorphism is a tricky kettle of fish for modern type theory.
> However my naive approach (which works really well) is to rename
> generic variables as I go, and defining forall qualification to be on
> the inner-most function that is possible.
> 
> I solved the "dup apply" (or "dup i", god I hate using "i" to mean
> application) problem by reintroducing "self" types.

In Joy at least, the i combinator does not mean application. Joy is a
concatenative language, not an applicative language. The applicative
languages are the lambda calculus and the combinatory calculus,
together with their descendents ­ just about all programming languages
descend from the lambda calculus. All applicative languages  have an
apply operation: apply this function to those arguments, but mostly there
is no explicit symbol for that operation. Joy does not have such an
operation
neither explicit nor implicit.

The i combinator in Joy is pretty much the same as the eval function in
Lisp. It undoes what the the (pseudo-) function quote does. In Lisp this
is true about expressions X (which denote objects):


> (eval(quote(X)) = X

And in Joy this is true about expressions X (which denote
stack-to-stack functions)

> [X] i = X

so the i combinator undoes what the quotation brackets do. Lisp¹s eval
and Joy¹s i are sometimes called dequotation operators. But they are
quite different from application. (Many books on Lisp have an example
program which is a Lisp interpreter written in Lisp. The two principal
parts are eval and apply ‹ and they are very different.)

All other Joy combinators are variations on the eval-theme. Some
enterprising Lisp programmer might write variations on the eval-theme
in Lisp ­ at least for those combinators that do not depend on Joy¹s
stack semantics. One example would be a map-eval, quite different
from the (second order) map function which many books will give as
examples.

  - Manfred 
 



[Non-text portions of this message have been removed]