# Concatenative Research

## Justin — 2011-01-31 00:20:55

    Hello. Is this forum still alive? I haven't shown my head here for a couple of years. I'm a MA/CS major with an ongoing interest in giving concatenative languages a firmer mathematical foundation. I have a few partial results: (i) an operational semantics, (ii) a concept of & application for homomorphisms, (iii) a type system. Is anyone else around here interested in this sort of research? Here's a link to my (ongoing) work,

    http://dl.dropbox.com/u/17328602/concat/index.html

## William Tanksley, Jr — 2011-01-31 01:23:40

    Justin <zallambo@...> wrote:

     > Hello. Is this forum still alive?

     Well... it is not dead which can eternal lie.

    I'm still actively working on some theory.

     > I haven't shown my head here for a couple of years. I'm a MA/CS major with an ongoing interest in giving concatenative languages a firmer mathematical foundation. I have a few partial results: (i) an operational semantics, (ii) a concept of & application for homomorphisms, (iii) a type system. Is anyone else around here interested in this sort of research? Here's a link to my (ongoing) work,

    > http://dl.dropbox.com/u/17328602/concat/index.html

     Wow, that's pretty cool. Thank you!

    Others have suggested using "compositional language", and there's

    nothing wrong with that; but historically, it's already been used in a

    number of fields to describe other languages. In cognitive science,

    it's the ability for the brain to form languages out of multiple

    parts; in software engineering, a compositional language is a language

    designed to help components interoperate. I like "concatenative

    language" not only because it's not previously used in this field, but

    also because it nicely describes the syntax of the language, and

    syntax is a crucial part of a language's description.

    I'm currently working on exploring a useless nook of concatenative

    languages that I called "completely flat languages". A completely flat

    concatenative language is defined not only by being concatenative

    (that is, any two valid programs can be concatenated to form a valid

    program), but also by being completely flat -- there is no discernible

    syntactic structure. This means that every bitstring is a valid

    program, and a program can be cut at any location to produce two valid

    programs the composition of whose semantics is the original program's

    semantics.

    Naturally, I reduced this to the single-bit case: a language with only

    two words, "0" and "1". "0" pushes some quotations on the stack, and

    "1" pops and executes things from the stack. I'm currently using the

    "k" combinator for "1", and usually "0" is something like "[], [cake],

    [k]". (See Kerby's definitions of common combinators on

    http://tunes.org/~iepos/joy.html#cakek for explanations.)

    I fairly easily built a brute force searcher for combinators in the 01

    language (integers map to all possible programs, so brute force is a

    simple search), then I added two interesting types of pruning (took me

    years to track down the last bug I fixed), and just a few months ago

    completed it. I just (this month) added a genetic algorithm to search

    for "better" definitions for "0", after which I ran into problems with

    my brute force searcher (I can compare combinators, but I don't

    properly compare quoted combinators). We'll see what happens...

    Your typechecker may well be useful, and your theory looks in line

    with what little I know. What license is your code under?

    My code's at https://bitbucket.org/wtanksleyjr/tworing, under GPL.

    Python, just like yours.

    -Wm

## John Cowan — 2011-01-31 02:41:58

    William Tanksley, Jr scripsit:

     > Well... it is not dead which can eternal lie.

     See my .sig.

    (Someone once asked me if such open references were safe.  I replied

    that I'm from New Jersey, where the very school lunches are made from

    shoggoth meat, and that I now lived in New York City, where we were

    foreclosing on R'lyeh the very next week.)

    --

    La mayyitan ma qadirun yatabaqqa sarmadi                            John Cowan

    Fa idha yaji' al-shudhdhadh fa-l-maut qad yantahi.              cowan@...

                    --Abdullah al-Hazred, Al-`Azif      http://www.ccil.org/~cowan

## Justin — 2011-01-31 05:11:06

    --- In concatenative@yahoogroups.com, "William Tanksley, Jr" <wtanksleyjr@...> wrote:

     > Others have suggested using "compositional language", and there's

    > nothing wrong with that; but historically, it's already been used in a

    > number of fields to describe other languages. In cognitive science,

    > it's the ability for the brain to form languages out of multiple

    > parts; in software engineering, a compositional language is a language

    > designed to help components interoperate. I like "concatenative

    > language" not only because it's not previously used in this field, but

    > also because it nicely describes the syntax of the language, and

    > syntax is a crucial part of a language's description.

     Alright, 'concatenative' it is.

     > I'm currently working on exploring a useless nook of concatenative

    > languages that I called "completely flat languages". A completely flat

    > concatenative language is defined not only by being concatenative

    > (that is, any two valid programs can be concatenated to form a valid

    > program), but also by being completely flat -- there is no discernible

    > syntactic structure. This means that every bitstring is a valid

    > program, and a program can be cut at any location to produce two valid

    > programs the composition of whose semantics is the original program's

    > semantics.

    >

    > Naturally, I reduced this to the single-bit case: a language with only

    > two words, "0" and "1". "0" pushes some quotations on the stack, and

    > "1" pops and executes things from the stack. I'm currently using the

    > "k" combinator for "1", and usually "0" is something like "[], [cake],

    > [k]". (See Kerby's definitions of common combinators on

    > http://tunes.org/~iepos/joy.html#cakek for explanations.)

     If "1" executes things from the stack, then it's undefined on an empty stack. And if it behaves differently on an empty stack than it does otherwise, you'll lose the concatenative property. How do you get around this?

     > Your typechecker may well be useful, and your theory looks in line

    > with what little I know. What license is your code under?

     Merely copyrighted, till I decide between a BSD-style and GPL-style licence. Recommendations?

     > My code's at https://bitbucket.org/wtanksleyjr/tworing, under GPL.

    > Python, just like yours.

     I was using Haskell at first, but my type inferencer is conspicuously stateful, and I couldn't figure out how to type it.

## William Tanksley, Jr — 2011-01-31 21:30:47

    Justin <zallambo@...> wrote:

     > "William Tanksley, Jr" <wtanksleyjr@...> wrote:

    >> Naturally, I reduced this to the single-bit case: a language with only

    >> two words, "0" and "1". "0" pushes some quotations on the stack, and

    >> "1" pops and executes things from the stack. I'm currently using the

    >> "k" combinator for "1", and usually "0" is something like "[], [cake],

    >> [k]". (See Kerby's definitions of common combinators on

    >> http://tunes.org/~iepos/joy.html#cakek for explanations.)

    > If "1" executes things from the stack, then it's undefined on an empty stack. And if it behaves differently on an empty stack than it does otherwise, you'll lose the concatenative property. How do you get around this?

     That's a runtime error, not a syntax error. And any word that takes

    ANY parameters behaves differently on different stacks; that's the

    purpose of taking parameters. :-)

     >> Your typechecker may well be useful, and your theory looks in line

    >> with what little I know. What license is your code under?

    > Merely copyrighted, till I decide between a BSD-style and GPL-style licence. Recommendations?

     I picked GPL at random. If you decide on BSD I'll happily switch to that.

     >> My code's at https://bitbucket.org/wtanksleyjr/tworing, under GPL.

    >> Python, just like yours.

    > I was using Haskell at first, but my type inferencer is conspicuously

    > stateful, and I couldn't figure out how to type it.

     A Haskell programmer. You're smarter than I am, then. :-)

    -Wm

## Justin — 2011-01-31 23:36:01

    --- In concatenative@yahoogroups.com, "William Tanksley, Jr" <wtanksleyjr@...> wrote:

     >

    > Justin <zallambo@...> wrote:

    > > "William Tanksley, Jr" <wtanksleyjr@> wrote:

    > >> I'm currently working on exploring a useless nook of concatenative

    > >> languages that I called "completely flat languages". A completely flat

    > >> concatenative language is defined not only by being concatenative

    > >> (that is, any two valid programs can be concatenated to form a valid

    > >> program), but also by being completely flat -- there is no discernible

    > >> syntactic structure. This means that every bitstring is a valid

    > >> program, and a program can be cut at any location to produce two valid

    > >> programs the composition of whose semantics is the original program's

    > >> semantics.

    > >>

    > >> Naturally, I reduced this to the single-bit case: a language with only

    > >> two words, "0" and "1". "0" pushes some quotations on the stack, and

    > >> "1" pops and executes things from the stack. I'm currently using the

    > >> "k" combinator for "1", and usually "0" is something like "[], [cake],

    > >> [k]". (See Kerby's definitions of common combinators on

    > >> http://tunes.org/~iepos/joy.html#cakek for explanations.)

    >

    > > If "1" executes things from the stack, then it's undefined on an empty stack. And if it behaves differently on an empty stack than it does otherwise, you'll lose the concatenative property. How do you get around this?

    >

    > That's a runtime error, not a syntax error. And any word that takes

    > ANY parameters behaves differently on different stacks; that's the

    > purpose of taking parameters. :-)

     Mm, I realize now that as I was thinking about your stated goal, I didn't have a precise definition of 'semantics' in mind. Would you agree with me that a semantics is a partial function from states to states, where in this case the state is a stack of quotations? (They must be _partial_ functions because they can (i) encounter runtime errors, and (ii) fail to halt.)

     > A Haskell programmer. You're smarter than I am, then. :-)

     Only until you learn Haskell :-). I highly recommend it.

## John Nowak — 2011-02-01 00:16:59

    On Jan 30, 2011, at 7:20 PM, Justin wrote:

     > I have a few partial results: (i) an operational semantics,

     The semantics are quite simple, aren't they?

     - juxtaposition is just function composition

     - all functions operate on lists (e.g. dup = \s@(x:_) -> x:s)

     - quotation of 'f' is just '(:) f'

     > (iii) a type system

     Typing a concatenative language is straightforward. You introduce a new kind 'Stack_K' and an inductively-defined type 'Stack' of kind 'Stack_K' that's either 'Empty' or a 'Cons' of a value with kind '*' and another 'Stack'. Your arrow constructor then has kind 'Stack_K -> Stack_K -> *' and quotation is kinded '* -> *' with type 'forall a b (c :: Stack_K). (a -> b) -> c -> Cons (a -> b) c'.

    - jn

## John Carter — 2011-02-01 21:02:22

    On Mon, Jan 31, 2011 at 6:11 PM, Justin <zallambo@...> wrote:

     >

    >

    > > What may be interesting and useful would be to return to typed variables

    > > (named values variety) and something like a SQL "natural join".

    >

    > I don't know what you mean. Could you give an example? (I don't have a good

    > mental model of databases.)

    >

     The truely irritating thing about both stack languages, and the more

    traditional languages with named parameters, is that the order of the

    parameters and the names don't really matter.

    Given any program P in a stack or traditional language, you can reorder

    and/or rename the parameters of every function anyway you choose... and come

    up with another program that does EXACTLY the same thing, so long as you

    carry through the renaming through the the body of each function and the

    reordering into every invocation of the function.

    In stack languages without parameter names, your program will _look_

    radically different as there will be a flock of stack manipulation operators

    different.

    ie. In a very strong sense, parameter names and parameter order is fluff and

    irrelevant to the actual computation being performed!

    Thus my mathematical gut feeling is, one should be able to eliminate it

    _all_ in some representation.

    I could be unconstructive an give you a lmgtfy link about natural joins, but

    let me rather discard the SQLish analogy and try say what I mean in a

    stackish language.

    Well, a lot of stack languages (Factor is a very good example) give the

    stack effect for each function as something like...

    fn: T1, T2, T3... -> T4, T5... where I mean fn is a function that pops

    parameters of type ..., T3, T2, T1 off the stack, in that order and pushes

    objects of type T4, T5, .. onto the stack in that order.

    Well, lets add some names...

    fn: i1 T1, i2 T2, ...-> o4 T4, o5 T5, ...

    Where I am naming my input parameters i1, i2, ... and my output values as

    o4, o5, ...

    Now a fragment of any stack language code tends to look like....

      fn1 stackOp1 stackOp2, ... fn2

    where all the stackOps rearrange the stack as it was left by fn1 and it's

    predecessors, so as to feed fn2 correctly.

    However, it you were to look at the stack effect declarations for fn1, and

    fn2, it would probably be obvious from the types alone, as which stackOps

    you would need between fn1 and fn2!

    And if the types alone weren't enough to tell you, the names certainly

    would!

    Thus in principle one could create a language where you could write a

    fragment as fn1 fn2 and the compiler could infer what stackOps (or calling

    parameters and their order) are required.

    --

    John Carter                             Phone : (64)(3) 358 6639

    Tait Electronics                        Fax   : (64)(3) 359 4632

    PO Box 1645 Christchurch                Email : john.carter@...

    New Zealand

    =======================================================================

    This email, including any attachments, is only for the intended

    addressee.  It is subject to copyright, is confidential and may be

    the subject of legal or other privilege, none of which is waived or

    lost by reason of this transmission.

    If the receiver is not the intended addressee, please accept our

    apologies, notify us by return, delete all copies and perform no

    other act on the email.

    Unfortunately, we cannot warrant that the email has not been

    altered or corrupted during transmission.

    =======================================================================

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

## John Cowan — 2011-02-01 22:56:07

    John Carter scripsit:

     > ie. In a very strong sense, parameter names and parameter order is fluff and

    > irrelevant to the actual computation being performed!

     Well, either is dispensible given the other, but you can't get rid of both,

    as many functions are not commutative.

     > However, it you were to look at the stack effect declarations for fn1, and

    > fn2, it would probably be obvious from the types alone, as which stackOps

    > you would need between fn1 and fn2!

     Only if you don't need to support subtraction.

     > Thus in principle one could create a language where you could write a

    > fragment as fn1 fn2 and the compiler could infer what stackOps (or calling

    > parameters and their order) are required.

     Scheme compilers actually do rearrange the argument order when all calling

    points are known.

    --

    So they play that [tune] on                     John Cowan

    their fascist banjos, eh?                       cowan@...

            --Great-Souled Sam                      http://www.ccil.org/~cowan

## Justin — 2011-02-02 02:22:23

    --- In concatenative@yahoogroups.com, John Nowak <john@...> wrote:

     >

    >

    > On Jan 30, 2011, at 7:20 PM, Justin wrote:

    >

    > > I have a few partial results: (i) an operational semantics,

    >

    > The semantics are quite simple, aren't they?

    >

    >  - juxtaposition is just function composition

    >  - all functions operate on lists (e.g. dup = \s@(x:_) -> x:s)

    >  - quotation of 'f' is just '(:) f'

     Except that you have not dealt with runtime exceptions (e.g. stack underflow) or program non-termination.

     > > (iii) a type system

    >

    > Typing a concatenative language is straightforward. You introduce a new kind 'Stack_K' and an inductively-defined type 'Stack' of kind 'Stack_K' that's either 'Empty' or a 'Cons' of a value with kind '*' and another 'Stack'. Your arrow constructor then has kind 'Stack_K -> Stack_K -> *' and quotation is kinded '* -> *' with type 'forall a b (c :: Stack_K). (a -> b) -> c -> Cons (a -> b) c'.

     Aha, that is a good way of looking at it. Have you written anything along these lines? I would be interested in reading it.

    My type system also has polymorphic data types (not too unusual), and what I'll call "cyclic types". A cyclic type is one that violates the occurs check and refers to itself. For instance, the correct type of 'dup apply' is

      (A x -> B), with x = (A x -> B)

    Notice that x occurs in its own definition.

    Christopher Diggin's type system for Cat is actually very close to this, but it doesn't admit polymorphic types (as far as I'm aware), and I don't think it handles cyclic types correctly. Cat's type inferencer gives the correct type for 'dup apply',

      (A (A self -> B) -> B)

    But on the program 'dup dig dup bury true bury if', it gives the type,

      (A (A (self -> B) self -> B) (A self (self -> B) -> B) -> B)

    First, there is ambiguity as to which enclosing quotation each 'self' refers to. Second, there seems to be a kind error in the subexpression '(self -> B)'. Like you said, '->' has kind 'Stack_K -> Stack_K -> *'. But 'self' has kind '*', unless I am mistaken. Any thoughts?

    The type I get (by hand; it's easy enough to verify) is

      (A (S -> B) (S -> B) -> B, with S = A (S -> B) (S -> B)

## Don Groves — 2011-02-02 04:20:48

    On 1 Feb 2011, at 13:02, John Carter wrote:

     > On Mon, Jan 31, 2011 at 6:11 PM, Justin <zallambo@...> wrote:

    >

    > >

    > >

    > > > What may be interesting and useful would be to return to typed variables

    > > > (named values variety) and something like a SQL "natural join".

    > >

    > > I don't know what you mean. Could you give an example? (I don't have a good

    > > mental model of databases.)

    > >

    >

    > The truely irritating thing about both stack languages, and the more

    > traditional languages with named parameters, is that the order of the

    > parameters and the names don't really matter.

    >

    > Given any program P in a stack or traditional language, you can reorder

    > and/or rename the parameters of every function anyway you choose... and come

    > up with another program that does EXACTLY the same thing, so long as you

    > carry through the renaming through the the body of each function and the

    > reordering into every invocation of the function.

    >

    > In stack languages without parameter names, your program will _look_

    > radically different as there will be a flock of stack manipulation operators

    > different.

    >

    > ie. In a very strong sense, parameter names and parameter order is fluff and

    > irrelevant to the actual computation being performed!

    >

    > Thus my mathematical gut feeling is, one should be able to eliminate it

    > _all_ in some representation.

    >

    > I could be unconstructive an give you a lmgtfy link about natural joins, but

    > let me rather discard the SQLish analogy and try say what I mean in a

    > stackish language.

    >

    > Well, a lot of stack languages (Factor is a very good example) give the

    > stack effect for each function as something like...

    >

    > fn: T1, T2, T3... -> T4, T5... where I mean fn is a function that pops

    > parameters of type ..., T3, T2, T1 off the stack, in that order and pushes

    > objects of type T4, T5, .. onto the stack in that order.

    >

     Given only this, shouldn't the inner interpreter be able to perform stack shuffling between function calls automatically?

    --

    don

     >

    > Well, lets add some names...

    >

    > fn: i1 T1, i2 T2, ...-> o4 T4, o5 T5, ...

    >

    > Where I am naming my input parameters i1, i2, ... and my output values as

    > o4, o5, ...

    >

    > Now a fragment of any stack language code tends to look like....

    >

    > fn1 stackOp1 stackOp2, ... fn2

    >

    > where all the stackOps rearrange the stack as it was left by fn1 and it's

    > predecessors, so as to feed fn2 correctly.

    >

    > However, it you were to look at the stack effect declarations for fn1, and

    > fn2, it would probably be obvious from the types alone, as which stackOps

    > you would need between fn1 and fn2!

    >

    > And if the types alone weren't enough to tell you, the names certainly

    > would!

    >

    > Thus in principle one could create a language where you could write a

    > fragment as fn1 fn2 and the compiler could infer what stackOps (or calling

    > parameters and their order) are required.

    >

    > --

    > John Carter Phone : (64)(3) 358 6639

    > Tait Electronics Fax : (64)(3) 359 4632

    > PO Box 1645 Christchurch Email : john.carter@...

    > New Zealand

    >

    > =======================================================================

    > This email, including any attachments, is only for the intended

    > addressee. It is subject to copyright, is confidential and may be

    > the subject of legal or other privilege, none of which is waived or

    > lost by reason of this transmission.

    > If the receiver is not the intended addressee, please accept our

    > apologies, notify us by return, delete all copies and perform no

    > other act on the email.

    > Unfortunately, we cannot warrant that the email has not been

    > altered or corrupted during transmission.

    > =======================================================================

    >

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

    >

    >

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

## John Nowak — 2011-02-02 09:41:37

    On Feb 1, 2011, at 9:22 PM, Justin wrote:

     > --- In concatenative@yahoogroups.com, John Nowak <john@...> wrote:

    >

    >> - juxtaposition is just function composition

    >> - all functions operate on lists (e.g. dup = \s@(x:_) -> x:s)

    >> - quotation of 'f' is just '(:) f'

    >

    > Except that you have not dealt with runtime exceptions (e.g. stack underflow) or program non-termination.

     Sure, but there's no reason any special work needs to be done for concatenative languages, is there? Concatenative languages have the same bottom-preserving semantics any partial higher-order language with eager evaluation and lambda abstractions would have.

    I guess my point is that you can see concatenative languages as "just" your usual higher-order eager language with a different syntax for composition and lambda abstraction (e.g. '[f g] == (:) (\s -> (g . f) s)', with the eta-expansion there to delay evaluation). Since the difference is simply syntax, I'm not sure why the semantics would require special treatment.

    I should mention that I assume quotations form a proper opaque abstraction (as in lambda calculus) and are not dissectible (as in Joy). My above semantics for quotation doesn't work for Joy and instead describing the semantics for 'i' would be the interesting part. I've been on the record many times now though as saying those semantics are undesirable for a programming language; the ability to form new abstractions is critical.

     >> Typing a concatenative language is straightforward. You introduce a new kind 'Stack_K' and an inductively-defined type 'Stack' of kind 'Stack_K' that's either 'Empty' or a 'Cons' of a value with kind '*' and another 'Stack'. Your arrow constructor then has kind 'Stack_K -> Stack_K -> *' and quotation is kinded '* -> *' with type 'forall a b (c :: Stack_K). (a -> b) -> c -> Cons (a -> b) c'.

    >

    > Aha, that is a good way of looking at it. Have you written anything along these lines? I would be interested in reading it.

     I've not, although I probably should before someone else does! Then again, there are only about 3 people interested in this problem...

     > My type system also has polymorphic data types (not too unusual), and what I'll call "cyclic types". A cyclic type is one that violates the occurs check and refers to itself. For instance, the correct type of 'dup apply' is

    >  (A x -> B), with x = (A x -> B)

    > Notice that x occurs in its own definition.

     I think the cyclic types you're proposing, commonly called "equirecursive types", are unnecessary. The 'dup apply' combinator is basically equivalent to the 'm' combinator in lambda calculus (i.e. '\x -> x x'). This is ill-typed in most typed systems. O'Caml will permit it with the "-rectypes" flag (which enables equirecursive types), but that flag is disabled by default and for good reason: It adds little utility and makes for some ugly type errors.

     > Christopher Diggin's type system for Cat is actually very close to this, but it doesn't admit polymorphic types (as far as I'm aware), and I don't think it handles cyclic types correctly.

     I'm not sure that Diggins has a sound system. As you've discovered, it returns some strange results.

    If you're interested in typing combinators like 'dup apply', I think intersection types are a more interesting approach:

       dup apply : for all a b c d. Cons ((b -> c) /\ (Cons (b -> c) a -> d)) a -> d

    If you read that carefully, it should make sense. I believe Slava put the basis of the idea in my head originally. Of course, the problem with this approach is that you now have intersection types to contend with.  Again, for a practical system, I don't think it's worth it.

    The last thing I'll point out with respect to the type system is that, due to recursive function calls working on a list that represents the entire program state (and not just its "arguments"), you have quite a lot of polymorphic recursion; any recursive function where the recursive call occurs on a stack that has "grown" is polymorphic recursive. You could try to infer some cases of this (Milner-Mycroft), but the problem is undecidable in general. I think requiring type signatures on many recursive functions would therefore be a requirement. It's not one that I consider particularly onerous however.

    - jn

## John Nowak — 2011-02-02 10:02:57

    On Feb 1, 2011, at 4:02 PM, John Carter wrote:

     > The truely irritating thing about both stack languages, and the more

    > traditional languages with named parameters, is that the order of the

    > parameters and the names don't really matter.

    >

    > ...

    >

    > ie. In a very strong sense, parameter names and parameter order is fluff and

    > irrelevant to the actual computation being performed!

     You could have functions of multiple arguments take records instead. That does away with your parameter names (as you can use field accessors internally) and therefore all substitution, renaming, and the usual lambda dance. It also does away with your argument ordering.

    Programming in such a way would work fairly well in a language like Backus's FP. To echo Tanksley, it's lovely. If you've not read Backus's Turing Award lecture, you must: http://www.stanford.edu/class/cs242/readings/backus.pdf

    That said, I take issue with the charge that these names are all just fluff. Pointfree languages are generally bad at using a single value at multiple places within a computation. Variables make this much easier.

    Pointfree languages are also generally *very* bad at refactoring. This may seem like a strange charge when you have languages with names like "Factor", but it's true. Take, for example, the following function (in pseudo-Joy) that sums a list:

        sum = [0] dip [null?] [drop] [uncons [+] dip sum] ifte

    Now take that and refactor it to a generic fold function that abstracts over the initializer (in this case '0') and the function to fold with (in this case '+'). In a language with variables, this is trivial. For example, I might do something like this:

        Z F fold = [Z] dip [null?] [drop] [uncons F dip sum] ifte

    Without variables, this isn't pretty. I'll leave it as a fun exercise.

    - jn

## William Tanksley, Jr — 2011-02-02 18:47:04

    John Nowak <john@...> wrote:

     > John Carter wrote:

    >> ie. In a very strong sense, parameter names and parameter order is fluff and

    >> irrelevant to the actual computation being performed!

    > You could have functions of multiple arguments take records instead. That does

    > away with your parameter names (as you can use field accessors internally)

    > and therefore all substitution, renaming, and the usual lambda dance. It also

    > does away with your argument ordering.

     Done the easy way this results in one record per complex function;

    done the complex way it results in a sophisticated structural

    hierarchy in your API. Neither one is inherently bad (it seems to me),

    it just has different costs and benefits. Of course, for a language to

    claim to support this it should provide some syntactic support beyond

    simply allowing it :-).

    Factor has some very simple support for this style, but the resulting

    code takes more room than stack manipulations. OTOH, it's almost

    certainly clearer what's going on for those parts of the API that use

    it (because they have complex inputs and outputs).

    Some other ideas occur to me, but this feels like the wrong place for

    brainstorming details like that.

     > That said, I take issue with the charge that these names are all just fluff.

     I have to completely agree. Less strongly, "parameter names and

    parameter order" cannot both be fluff at the same time.

     > Pointfree languages are generally bad at using a single value at multiple

    > places within a computation. Variables make this much easier.

     A better term is "less powerful" rather than "bad". I don't say that

    out of a mere political correctness; the idea of power can be

    formalized to show its good and bad sides. Informally, variable names

    allow the programmer to teleport data around. The new power tempts the

    programmer to increase the scope available for its use, making

    functions tend to be larger (since modern languages are lexically

    scoped).

    Once you start down that path, forever will it dominate your destiny.

    Consume you it will. (Yoda is, after all, the patron saint of stack

    programmers.)

    And, more seriously, I do recognize that power is good. But next you

    give an example where power is bad:

     > Pointfree languages are also generally *very* bad at refactoring.

    > This may seem like a strange charge when you have languages

    > with names like "Factor", but it's true.

     You're basically right -- higher-order point-free functional languages

    are in general harder to refector, because they tend to have a lot of

    broad syntactic structure. The less powerful lower-order concatenative

    languages like Forth tend to be easier to refactor, although they have

    their own problems abundantly.

     > - jn

     -Wm

## Justin — 2011-02-03 10:52:05

    --- In concatenative@yahoogroups.com, John Nowak <john@...> wrote:

     > I guess my point is that you can see concatenative languages as "just" your usual higher-order eager language with a different syntax for composition and lambda abstraction (e.g. '[f g] == (:) (\s -> (g . f) s)', with the eta-expansion there to delay evaluation). Since the difference is simply syntax, I'm not sure why the semantics would require special treatment.

     You might be right. In fact, it may follow that my semantics can be thought of in terms of the lambda calculus. I'll ponder that. But couldn't one also view the concatenative calculus as an alternative to the lambda calculus which may in some circumstances prove more elegant? After all, there's no variables (and the accompanying alpha-renaming), no function application (and the accompanying order-of-evaluation questions), and even no function abstraction if you don't want it.

     > I should mention that I assume quotations form a proper opaque abstraction (as in lambda calculus) and are not dissectible (as in Joy). My above semantics for quotation doesn't work for Joy and instead describing the semantics for 'i' would be the interesting part. I've been on the record many times now though as saying those semantics are undesirable for a programming language; the ability to form new abstractions is critical.

     Agreed! Quotations should be opaque, functions should be unable to gauge the depth of the stack, and functions should be unable to discern anything about the parts of the program following them.

     > >> Typing a concatenative language is straightforward. You introduce a new kind 'Stack_K' and an inductively-defined type 'Stack' of kind 'Stack_K' that's either 'Empty' or a 'Cons' of a value with kind '*' and another 'Stack'. Your arrow constructor then has kind 'Stack_K -> Stack_K -> *' and quotation is kinded '* -> *' with type 'forall a b (c :: Stack_K). (a -> b) -> c -> Cons (a -> b) c'.

    > >

    > > Aha, that is a good way of looking at it. Have you written anything along these lines? I would be interested in reading it.

    >

    > I've not, although I probably should before someone else does! Then again, there are only about 3 people interested in this problem...

     Here, I've just written something up on types & kinds. It's based on your suggestion, in conjunction with what I had been thinking when I wrote the type inferencer.

    http://dl.dropbox.com/u/17328602/concat/lang//medium/algorithm/types.pdf

     > I think the cyclic types you're proposing, commonly called "equirecursive types", are unnecessary. The 'dup apply' combinator is basically equivalent to the 'm' combinator in lambda calculus (i.e. '\x -> x x'). This is ill-typed in most typed systems. O'Caml will permit it with the "-rectypes" flag (which enables equirecursive types), but that flag is disabled by default and for good reason: It adds little utility and makes for some ugly type errors.

     And here I was thinking that "cyclic types" hadn't been well-studied.

     > If you're interested in typing combinators like 'dup apply', I think intersection types are a more interesting approach:

    >

    >    dup apply : for all a b c d. Cons ((b -> c) /\ (Cons (b -> c) a -> d)) a -> d

    >

    > If you read that carefully, it should make sense. I believe Slava put the basis of the idea in my head originally. Of course, the problem with this approach is that you now have intersection types to contend with.  Again, for a practical system, I don't think it's worth it.

     That certainly works. Do you know which is more powerful, equirecursive or intersection types?

     > The last thing I'll point out with respect to the type system is that, due to recursive function calls working on a list that represents the entire program state (and not just its "arguments"), you have quite a lot of polymorphic recursion; any recursive function where the recursive call occurs on a stack that has "grown" is polymorphic recursive. You could try to infer some cases of this (Milner-Mycroft), but the problem is undecidable in general. I think requiring type signatures on many recursive functions would therefore be a requirement. It's not one that I consider particularly onerous however.

     Wait, are you saying that typing a typical concatenative language (which allows functions to recursively grow the data stack) is undecidable?

## William Tanksley, Jr — 2011-02-03 15:26:46

    Justin <zallambo@...> wrote:

     > Wait, are you saying that typing a typical concatenative language (which allows functions to recursively grow the data stack) is undecidable?

     Typing is inherently undecidable. That's one of the fundamental

    results of computer science.

    -Wm

## John Cowan — 2011-02-03 16:39:58

    William Tanksley, Jr scripsit:

     > Typing is inherently undecidable. That's one of the fundamental

    > results of computer science.

     Well, sufficiently general typing is undecidable.  Hindley-Milner typing

    isn't undecidable, it's just a straitjacket.

    Consider the function x defined by the following cases:

    x true true = true;

    x _ false = false;

    x false _ = false;

    where _ is "don't care".  Under H-M typing, this is an AND function, and

    its type is bool -> bool -> bool.  But the actual function allows a lot

    more than that!  For example, x foo false is defined, and so is x false

    bar, though x foo bar is not defined.  So the H-M type overconstrains

    the function.

    Success typing, as used in Erlang's Dialyzer, comes up with the much

    more reasonable type any -> any -> bool, where any is a union of all

    the available types.  It's quite decidable, and has the advantage that

    it never reports a type error unless there is a definite clash (like

    passing the wrong type to a built-in).

    --

    They tried to pierce your heart                 John Cowan

    with a Morgul-knife that remains in the         http://www.ccil.org/~cowan

    wound.  If they had succeeded, you would

    become a wraith under the domination of the Dark Lord.         --Gandalf

## John Cowan — 2011-02-03 18:41:11

    Justin scripsit:

     > Agreed! Quotations should be opaque, functions should be unable to

    > gauge the depth of the stack, and functions should be unable to discern

    > anything about the parts of the program following them.

     *sigh*

    The minute anyone gets a hold of the Joy model, the first thing they ditch

    is the beautiful code/data duality.  It is IMHO part of the essence of

    Joy that you construct lists-as-code with the same mechanisms you use

    to construct lists of any sort, and the stack is just another list.

    (Lisp/Scheme tries to allow the former, but issues around lexical scope

    make it impossible in the general case: syntax objects are not lists

    and symbols.)  Sacrificing that beauty to the fashionable model of static

    typing strikes me as just sad.

    --

    John Cowan          http://www.ccil.org/~cowan         cowan@...

    The native charset of SMS messages supports English, French, mainland

    Scandinavian languages, German, Italian, Spanish with no accents, and

    GREEK SHOUTING.  Everything else has to be Unicode, which means you get

    nly 70 16-bit characters in a text instead of 160 7-bit characters.

## Justin — 2011-02-03 19:18:38

    --- In concatenative@yahoogroups.com, John Cowan <cowan@...> wrote:

     >

    > Justin scripsit:

    >

    > > Agreed! Quotations should be opaque, functions should be unable to

    > > gauge the depth of the stack, and functions should be unable to discern

    > > anything about the parts of the program following them.

    >

    > *sigh*

    >

    > The minute anyone gets a hold of the Joy model, the first thing they ditch

    > is the beautiful code/data duality.  It is IMHO part of the essence of

    > Joy that you construct lists-as-code with the same mechanisms you use

    > to construct lists of any sort, and the stack is just another list.

    > (Lisp/Scheme tries to allow the former, but issues around lexical scope

    > make it impossible in the general case: syntax objects are not lists

    > and symbols.)  Sacrificing that beauty to the fashionable model of static

    > typing strikes me as just sad.

     The code/data duality isn't being sacrificed on the altar of static typing; it's being sacrificed in the name of algebraic reasoning about programs. The ability to reason about how your code behaves comes not from what your language can do, but from what it can't. That being said, why not have both lists and quotations, and allow lists to be converted into quotations?

## stevan apter — 2011-02-03 19:25:44

    On Feb 3, 2011, at 1:41 PM, John Cowan wrote:

     > Justin scripsit:

    >

    > > Agreed! Quotations should be opaque, functions should be unable to

    > > gauge the depth of the stack, and functions should be unable to discern

    > > anything about the parts of the program following them.

    >

    > *sigh*

    >

    > The minute anyone gets a hold of the Joy model, the first thing they ditch

    > is the beautiful code/data duality. It is IMHO part of the essence of

    > Joy that you construct lists-as-code with the same mechanisms you use

    > to construct lists of any sort, and the stack is just another list.

    > (Lisp/Scheme tries to allow the former, but issues around lexical scope

    > make it impossible in the general case: syntax objects are not lists

    > and symbols.) Sacrificing that beauty to the fashionable model of static

    > typing strikes me as just sad.

    >

     not me!  that's the most beautiful aspect of joy.  in

    XY i provide two operators, enclose and disclose.  enclose

    of a quotation returns a function atom; disclose of a

    function atom returns a quotation.  as i argued back

    then, it's convenient to be able to "bottom out" at

    the function level in recursions over quotations whose

    outer structure is container-like and whose leaves are

    function-like.  of course, this distinction is entirely

    in the programmer's mind, but it's useful to be able to

    mark it in the code.

    	http://nsl.com/k/xy/xy.txt

    XY 0 is the last (and purest) version of this idea.

     >

    > --

    > John Cowan http://www.ccil.org/~cowan cowan@...

    > The native charset of SMS messages supports English, French, mainland

    > Scandinavian languages, German, Italian, Spanish with no accents, and

    > GREEK SHOUTING. Everything else has to be Unicode, which means you get

    > nly 70 16-bit characters in a text instead of 160 7-bit characters.

    >

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

## John Cowan — 2011-02-03 20:53:40

    Justin scripsit:

     > The code/data duality isn't being sacrificed on the altar of static

    > typing; it's being sacrificed in the name of algebraic reasoning about

    > programs. The ability to reason about how your code behaves comes not

    > from what your language can do, but from what it can't. That being

    > said, why not have both lists and quotations, and allow lists to be

    > converted into quotations?

     For one thing, every datum in Joy is also code; 3 is the integer 3, but

    also the function that accepts an arbitrary list and returns a list

    extended with a new element that is the integer 3.

    --

    But you, Wormtongue, you have done what you could for your true master.  Some

    reward you have earned at least.  Yet Saruman is apt to overlook his bargains.

    I should advise you to go quickly and remind him, lest he forget your faithful

    service.  --Gandalf             John Cowan <cowan@...>

## William Tanksley, Jr — 2011-02-04 03:51:32

    John Cowan <cowan@...> wrote:

     > William Tanksley, Jr scripsit:

    >> Typing is inherently undecidable. That's one of the fundamental

    >> results of computer science.

    > Well, sufficiently general typing is undecidable.  Hindley-Milner typing

    > isn't undecidable, it's just a straitjacket.

     My response was to a question asked about the phrase "You could try to

    infer some cases of this (Milner-Mycroft), but the problem is

    undecidable in general." This phrase is the true story of typechecking

    -- you can often find a special case, but usually the first place you

    look winds up not being very useful for actual programming.

     > They tried to pierce your heart                 John Cowan

     Look! Your quote just became an emo song.

    -Wm

## William Tanksley, Jr — 2011-02-04 04:38:57

    Justin <zallambo@...> wrote:

     > Agreed! Quotations should be opaque, functions

    > should be unable to gauge the depth of the stack,

    > and functions should be unable to discern anything

    > about the parts of the program following them.

     What I'd say is that programs tend to be less closely coupled together

    when they don't depend on the structure of the functions they call (or

    otherwise use); don't depend on data used by their callers; and don't

    depend on the structure of the source they're called from. (This is

    simply a rephrasing of what you've just said.)

    Is that a "should"? Only when the benefits exceed the costs.

    Many Forth programmers use its ability to look forward in their own

    source, and concatenative languages in general have that potential in

    a rather interesting manner. (Not "unique", mind you -- lazy languages

    can also look at their own source.) But when you DO that, you lose

    something as well.

    Gauging the depth of the stack seems like suicide -- but when you're

    running on a GA144 array, if you DON'T know, you're probably stepping

    on something important (your stacks are only 8 elements deep, and

    circular; you have two stacks per core, and 144 cores).

    I don't have a strong appeal in favor of non-opaque quotations; I

    don't find them to be immensely practical, but you have to admit that

    they're one of the fun features of Joy. Getting rid of them is boring.

    Replacing them with a separate function syntax and a conversion

    operator is OK, I guess... But hardly appealing.

    -Wm

## John Nowak — 2011-02-07 03:42:25

    On Feb 3, 2011, at 5:52 AM, Justin wrote:

     > But couldn't one also view the concatenative calculus as an alternative to the lambda calculus which may in some circumstances prove more elegant? After all, there's no variables (and the accompanying alpha-renaming), no function application (and the accompanying order-of-evaluation questions), and even no function abstraction if you don't want it.

     I think most people would agree that the machinery, if you will, is simpler. The SK calculus is also simpler.

    That said, I'm not sure it matters. What matters is how simply these things can be applied to particular problems. In that respect, it does seem that the power of substitution is hard to pass up.

     > That certainly works. Do you know which is more powerful, equirecursive or intersection types?

     Neither is more powerful than the other. The "power" of a system really depends on what you're trying to do with it.

     > Wait, are you saying that typing a typical concatenative language (which allows functions to recursively grow the data stack) is undecidable?

     No, type checking for such a language can be decidable. It's only type inference in the presence of polymorphic recursion that is not decidable. This is not at all unique to concatenative languages.

    - jn

## John Nowak — 2011-02-07 03:56:40

    On Feb 3, 2011, at 11:39 AM, John Cowan wrote:

     > William Tanksley, Jr scripsit:

    >

    >> Typing is inherently undecidable. That's one of the fundamental

    >> results of computer science.

    >

    > Well, sufficiently general typing is undecidable.

     What's "sufficiently general" typing here? I use type systems that are decidable and sufficiently general every day. In fact, I often use type systems to do generic programming in ways I can't without a type system (e.g. Haskell's type classes).

     > Consider the function x defined by the following cases:

    >

    > x true true = true;

    > x _ false = false;

    > x false _ = false;

    >

    > where _ is "don't care".  Under H-M typing, this is an AND function, and

    > its type is bool -> bool -> bool.  But the actual function allows a lot

    > more than that!

    >

    > For example, x foo false is defined, and so is x false

    > bar, though x foo bar is not defined.  So the H-M type overconstrains

    > the function.

    >

    > Success typing, as used in Erlang's Dialyzer, comes up with the much

    > more reasonable type any -> any -> bool, where any is a union of all

    > the available types.

     I'd rather have the HM type. It makes it clear in the type that the values I'm passing will be used only for their boolean properties. I don't think it's fair to say the type is "over-constrained" at all, even if you assume that all values in the language do have some sort of boolean property that can be assigned to them.

     > It's quite decidable, and has the advantage that it never reports a type error unless there is a definite clash (like passing the wrong type to a built-in).

     Firstly, I strongly doubt the type system that Dialyzer attempts to enforce is decidable. There may be a terminating algorithm for what Dialyzer does, but this doesn't mean it is complete with respect to the type system. If the choice is between decidability and completeness, choosing the former isn't much of an accomplishment. (Is there even a particular type system that Dialyzer is attempting to enforce? I'm not sure it makes sense to talk about decidability or completeness at all.)

    Secondly, a type system that is restricted to only reporting errors that would occur at runtime is, in my opinion, severely limited. I'd prefer a type system that can easily enforce properties that I can't enforce at runtime (e.g. all the fun things you can do with phantom types and the more advanced variations thereof).

    - jn

## John Nowak — 2011-02-07 04:08:29

    On Feb 3, 2011, at 1:41 PM, John Cowan wrote:

     > Justin scripsit:

    >

    >> Agreed! Quotations should be opaque, functions should be unable to

    >> gauge the depth of the stack, and functions should be unable to discern

    >> anything about the parts of the program following them.

    >

    > *sigh*

    >

    > The minute anyone gets a hold of the Joy model, the first thing they ditch

    > is the beautiful code/data duality. It is IMHO part of the essence of Joy

    > that you construct lists-as-code with the same mechanisms you use to

    > construct lists of any sort, and the stack is just another list.

     I don't think that's part of the essence of Joy. It has nothing to do with Manfred's goals... so far as I know. More on that later.

    In either case, why not simply offer an 'eval' function that converts a list to an opaque quotation? You can then choose whatever is appropriate based on the problem instead of being locked in to a language without the ability to form abstractions.

     > Sacrificing that beauty to the fashionable model of static typing strikes me as just sad.

     Referring to static typing as fashionable is silly. It's just the opposite nowadays if anything.

    Either way, it's not being "sacrificed" just for typing. The problem with non-opaque quotations is that they destroy equational reasoning. In a Joy program, can you replace 'swap drop' with 'nip'? The answer is, "it depends". It depends on if it's in a quotation or not, and if it is, if the quotation may, at some point, be manipulated as a list.

    The essence of Joy, in my opinion, is simple equational reasoning. Manfred talks a lot about Joy's "exceptionally simple algebra". That seems to be the whole point of it. The problem, however, is that the algebra just doesn't work because you can't safely manipulate programs. A language where there is not a single program manipulation you can always safely perform doesn't strike me as having a particularly simple algebra. Moreover, the side conditions you need to prove to be able to manipulate something are, in general, whole program semantic properties. At least with the lambda calculus, things like required alpha conversions are simple, local, syntactic issues.

    - jn

## John Nowak — 2011-02-07 04:15:06

    On Feb 3, 2011, at 10:51 PM, William Tanksley, Jr wrote:

     > John Cowan <cowan@...> wrote:

    >

    >> William Tanksley, Jr scripsit:

    >>

    >>> Typing is inherently undecidable. That's one of the fundamental

    >>> results of computer science.

    >>

    >> Well, sufficiently general typing is undecidable.  Hindley-Milner typing

    >> isn't undecidable, it's just a straitjacket.

    >

    > My response was to a question asked about the phrase "You could try to

    > infer some cases of this (Milner-Mycroft), but the problem is

    > undecidable in general." This phrase is the true story of typechecking

    > -- you can often find a special case, but usually the first place you

    > look winds up not being very useful for actual programming.

     On the contrary, Milner-Mycroft works very well in most cases. When it appears to not be terminating, you can "just" bail out and report the issue to the programmer. This may not be particularly pretty, but it's not at all clear to me that it isn't useful. For example, recent work on inferring types in the presence of GADTs depends crucially on Milner-Mycroft and is able to infer types for vastly more expressions than existing, decidable systems.

    The reason Milner-Mycroft hasn't been more heavily adopted is that there isn't much of a need for it. Most programmers using languages like Haskell are already comfortable with types and see them as an important form of checked documentation and a very useful means of constraining program behavior. Adding complexity to the language so that programmers can avoid a bit of typing (pun not intended) is usually a bad tradeoff.

    - jn

## John Cowan — 2011-02-07 04:40:52

    John Nowak scripsit:

     > What's "sufficiently general" typing here?

     What I meant was, if you generalize your type system enough, it eventually

    becomes Turing-complete (by the Curry-Howard correspondence), hence

    undecidable.  I think this is uncontroversial.  That's presumably more

    general than you actually want.

     > I'd rather have the HM type. It makes it clear in the type that the

    > values I'm passing will be used only for their boolean properties. I

    > don't think it's fair to say the type is "over-constrained" at all,

    > even if you assume that all values in the language do have some sort

    > of boolean property that can be assigned to them.

     The H-M type allows the function to accept only "true" and "false",

    whereas a dynamically typed system will accept much more.  In that sense

    H-M is over-constrained: it doesn't permit a vast number of calls to this

    procedure that will actually (in a dynamically typed language) succeed.

    H-M insists that you only pass argument that *cannot* cause a run-time

    error (though, BTW, nobody has types "integer" and "nonzero integer" and

    requires that the denominator of a division belongs to the latter type).

     > Firstly, I strongly doubt the type system that Dialyzer attempts to

    > enforce is decidable. There may be a terminating algorithm for what

    > Dialyzer does, but this doesn't mean it is complete with respect to the

    > type system. If the choice is between decidability and completeness,

    > choosing the former isn't much of an accomplishment. (Is there even a

    > particular type system that Dialyzer is attempting to enforce? I'm not

    > sure it makes sense to talk about decidability or completeness at all.)

     It's complete in the sense that it rejects all expressions that it can

    prove to be invariably unsound (that is, unsound no matter what happens

    at run time).  It's not complete in the sense that it fails to reject

    all expressions that are sometimes unsound.

    I don't know any meaning of "decidable" except "guaranteed to terminate",

    which it is.

     > Secondly, a type system that is restricted to only reporting errors

    > that would occur at runtime is, in my opinion, severely limited. I'd

    > prefer a type system that can easily enforce properties that I can't

    > enforce at runtime (e.g. all the fun things you can do with phantom

    > types and the more advanced variations thereof).

     Well, I have no problem with you having your preferences.  But the

    importance of success typing is that it shows that type systems can be

    useful even if they are not in the H-M (or M-W) family.

    --

    They do not preach                              John Cowan

      that their God will rouse them                cowan@...

        A little before the nuts work loose.        http://www.ccil.org/~cowan

    They do not teach

      that His Pity allows them                         --Rudyard Kipling,

        to drop their job when they damn-well choose.   "The Sons of Martha"

## John Cowan — 2011-02-07 04:45:31

    John Nowak scripsit:

     > I don't think that's part of the essence of Joy. It has nothing to do

    > with Manfred's goals... so far as I know. More on that later.

     I'm not sure that Reynolds's analyses had much to do with Peter Naur's

    intentions either.

     > In either case, why not simply offer an 'eval' function that converts a

    > list to an opaque quotation? You can then choose whatever is appropriate

    > based on the problem instead of being locked in to a language without

    > the ability to form abstractions.

     If I want opaque abstractions, I know where to find them.  As I said,

    Lisp tries to do without opaque abstractions but fails.  Other languages

    don't try.  Joy succeeds.

     > Referring to static typing as fashionable is silly. It's just the

    > opposite nowadays if anything.

     I don't mean among programmers, I mean among CS/PLT researchers.  See any

    given LtU.

     > Either way, it's not being "sacrificed" just for typing. The problem

    > with non-opaque quotations is that they destroy equational reasoning. In

    > a Joy program, can you replace 'swap drop' with 'nip'? The answer is,

    > "it depends". It depends on if it's in a quotation or not, and if it

    > is, if the quotation may, at some point, be manipulated as a list.

     Quite so.

    --

    The man that wanders far                        cowan@...

    from the walking tree                           http://www.ccil.org/~cowan

            --first line of a non-existent poem by:         John Cowan

## John Nowak — 2011-02-07 04:53:30

    On Feb 6, 2011, at 11:40 PM, John Cowan wrote:

     > John Nowak scripsit:

    >

    >> What's "sufficiently general" typing here?

    >

    > What I meant was, if you generalize your type system enough, it eventually

    > becomes Turing-complete (by the Curry-Howard correspondence), hence

    > undecidable.  I think this is uncontroversial.  That's presumably more

    > general than you actually want.

     Right, I agree. I may have misread. I thought you were claiming that a system that is sufficient for "real work" will be undecidable or something along those lines.

     > (though, BTW, nobody has types "integer" and "nonzero integer" and

    > requires that the denominator of a division belongs to the latter type).

     Well, languages with dependent types can and do.

     > It's complete in the sense that it rejects all expressions that it can

    > prove to be invariably unsound (that is, unsound no matter what happens

    > at run time).  It's not complete in the sense that it fails to reject

    > all expressions that are sometimes unsound.

    >

    > I don't know any meaning of "decidable" except "guaranteed to terminate",

    > which it is.

     Well, as I said, it does terminate. But an algorithm that is decidable yet incomplete and unsound isn't much of an accomplishment! Any algorithm can be made decidable by just bailing out after awhile. I wouldn't, therefore, claim this is a feature of Dialyzer. Any practical system will do this. When people talk about decidabaility, they usually are asking if something is guaranteed to terminate while implementing the complete rules of the system. I don't believe Dialyzer does (or can) do this.

     > Well, I have no problem with you having your preferences.  But the

    > importance of success typing is that it shows that type systems can be

    > useful even if they are not in the H-M (or M-W) family.

     Of course. The type system in Typed Scheme is particularly nice given its goals.

    - jn

## John Cowan — 2011-02-07 05:02:30

    John Nowak scripsit:

     > > (though, BTW, nobody has types "integer" and "nonzero integer" and

    > > requires that the denominator of a division belongs to the latter type).

    >

    > Well, languages with dependent types can and do.

     At the expense of being undecidable!

     > Of course. The type system in Typed Scheme is particularly nice given

    > its goals.

     FWIU, Dialyzer and Soft Scheme are close variants of each other.

    --

    I am expressing my opinion.  When my            John Cowan

    honorable and gallant friend is called,         cowan@...

    he will express his opinion.  This is           http://www.ccil.org/~cowan

    the process which we call Debate.                   --Winston Churchill

## John Nowak — 2011-02-07 05:23:07

    On Feb 7, 2011, at 12:02 AM, John Cowan wrote:

     > John Nowak scripsit:

    >

    >>> (though, BTW, nobody has types "integer" and "nonzero integer" and

    >>> requires that the denominator of a division belongs to the latter type).

    >>

    >> Well, languages with dependent types can and do.

    >

    > At the expense of being undecidable!

     Not necessarily. Total languages (or languages that otherwise separate non-terminating terms) can have decidable dependent type checking.

    Regardless, undecidability isn't necessarily much of a curse. Provided it works well most of the time and can hint to the programmer how to help it when it fails, an undecidable system type *inference* system may be perfectly acceptable. After all, it's a compile-time issue. I'd rather that than a system that always terminates but may fail to catch legitimate problems.

    Of course, a system without a decidable algorithm for type *checking* is a more severe problem that might cause some irritation. Still, it may work well enough in some instances. People do claim to use C++.

     >> Of course. The type system in Typed Scheme is particularly nice given

    >> its goals.

    >

    > FWIU, Dialyzer and Soft Scheme are close variants of each other.

     That may be. I don't know much about Dialyzer.

    Typed Racket (which is what I was thinking of -- not the older Soft Scheme system), however, isn't what I'd usually call a soft system. Programs with type errors are rejected and there's no way that it'll fail to notice a type error. (I'm unsure if you can force it to run the program anyway.) The only way a runtime type error can occur is if a Typed Racket program calls regular untyped Racket code. In this case, contracts are used to do dynamic enforcement. It's quite a clever system, although I'm unsure of its utility outside of pedagogy.

    Not telling you anything you don't already know probably. Just encouraging people to give Typed Racket a look.

    - jn

## Chris Double — 2011-02-07 20:51:05

    On Mon, Feb 7, 2011 at 5:53 PM, John Nowak <john@...> wrote:

     > > (though, BTW, nobody has types "integer" and "nonzero integer" and

    > > requires that the denominator of a division belongs to the latter type).

    >

    > Well, languages with dependent types can and do.

     ATS does for example. From the prelude:

      idiv {i,j:int | j <> 0}

      (i: int i, j: int j):<> int (i/j)

      overload / with idiv

    Chris.

    --

    http://www.bluishcoder.co.nz

## Ruurd — 2011-02-07 21:54:36

    Hi all,

    IMHO, the mission statement of Joy seems to have been the removal of names. In that it has succeeded. The latest addition has been condnestrec, making explicit recursion unnecessary in all cases.

    Also the impossibility of rewriting is not as bad as it looks.

    Suppose I DEFINE fib == [small] [] [pred dup pred] [+] binrec.

    Because all quotations are hardcoded, this can be rewritten to

    DEFINE fib == binrec(small; ;pred dup pred; +).

    But only if fib is at top level in the first place, like in: 10 fib.

    This new binrec( does not take parameters from the stack but from

    elsewhere (static memory, not the code stream); otherwise it behaves the same as binrec. Furthermore the parameters to binrec( are not quotations anymore, just terms.

    And that makes further quotation lifting possible.

    It requires an n-token lookahead m-pass translator, but I think it can be done (I have not tried yet).

    And yes, it is not rewriting within the language Joy; rather it is rewriting to another, while preserving the semantics of Joy.

    rw

     --- In concatenative@yahoogroups.com, John Nowak <john@...> wrote:

    > The essence of Joy, in my opinion, is simple equational reasoning. Manfred talks a lot about Joy's "exceptionally simple algebra". That seems to be the whole point of it. The problem, however, is that the algebra just doesn't work because you can't safely manipulate programs. A language where there is not a single program manipulation you can always safely perform doesn't strike me as having a particularly simple algebra. Moreover, the side conditions you need to prove to be able to manipulate something are, in general, whole program semantic properties. At least with the lambda calculus, things like required alpha conversions are simple, local, syntactic issues.

    >

    > - jn

    >

## chris glur — 2011-02-01 07:30:36

    > I am still considering spending a Phd researching this area.

    >  Motivation

     Good, the motivation should be stated up front.

    I fetched the cited http*tunes*, which I found I had already previously

    started reading. And this is 'how' it reads for me:

    ] 1. John was born ...; has size X shoes; has ...

    ] 2. Mary was born...;has size Y shoes; has ...

    ...

    ] 37. Peter was born...

    So by that stage I asked my self WHAT IS THE MOTIVATION?!

    Where is this leading?

    Haven't these people heard about what we learned in 60-70's

    *Top down design*, goal directed design.

    Computing is complex, and its tasks need a central/controlling plan, with

    the goal always in sight/mind - to keep focus.

    So I looked back to the TOC, and found the "Conclusion", which I hoped would

     state the goal/motivation.

    The 'Conclusion' section was missing.

    Why do you people want to torment me?!

     > My interest stems from a gut feeling that the compositional model is

    > more elegant than the applicative model.

     'gut feeling' ??!!

    AFAIK doing a PhD is not like 'I think I'll try a new flavour candy'.

    What is it with this "get your self a full featured browser and

     have a *BETTER EXPERIENCE*" feely-feely US talk.

    Have y'all/any read eg. Backus' ca. '78 analysis of HOW/WHY

    <compositional model is better than the applicative model>.

    And crucially we must define better.

    I define it as 'getting me more results, with less pain/effort' --

    in the long run, for the type of tasks that I do.

    The items listed under the 'Motivation' heading are good/interesting

    but need to be written as paths to pre-defined goals.

    Have you ever dealt with law people?  Very strange thinkers.

    But I've learned from them: this bloke wrote that "I shouldn't vague-out".

    We techies, conditioned by math-studies to not explicitly spell out each step

    of the inference chain, often leave too much unstated and fuzzy.

     > I have the impression that variables are a difficult concept to grasp.

     Our/techie problem is that if/why psychological/soft 'impressions' are valid,

    must FIRST be established.  Ie. our goal must be to satisfy HUMAN requirements.

    The goal must first be determined. The technical details of how to achieve

    the supposed-to-be pre-defined goal [ie. what's discussed here and in the

    other literature] is just detail. We are continually starting new journeys

    without having defined our destination.

    Like 'surfing is going nowhere, while waiting to fall off'.

     > We spend years teaching students about variables in math class, and even in

    > college many students have difficulty understanding that (lambda x. x) and

    > (lambda y.  y) are identical.  This is certainly a double-edged sword -

    > variables are a powerful reasoning aid - but I am nonetheless interested

    > in glimpsing a world free of variables.

     Admittedly psychology/cog-science is not hard science.

    But we need to state [up front] that eg. the fewer variables/names/concept

    that need to be carried/remembered the better.

    And eg. that being able to read 'linearly' [with no forward references] is

    less of a mental load. And the reasons why the successive refinement method is

    economical and effective. Etc .....

    I've only recently come to realise how economical [hence efficient] the:

    A -> B -> C -> D -> ... -> GOAL; style of programming is.

    And I'm annoyed that it's been hidden from me for decades by the unwillingness

    of those who were able to advocate and explain, to lead the way.

    A trivial example of this cascading/filtered programming style is:

     List all files in sub-dir ->

     less than N days old ->

     which contain the string <string1> ->

     and the string <string2> ->

     ...and the <stringN> ->

     goal: to find that file that you read last week about XYZ.

    For *nix-boys this is a one-liner.

    OTOH one-lining is immature look-ma-no-hands like.

    And if we can separate the unfortunate baroque and irregular syntax of *nix,

    we see the powerful/economical multistage-data-transformation programming

    method which has proven a success over decades.

    So, take the basic proven idea and clean it and refine it, is my advice.

    But first make or get a ready-made justification of well defined goals.

    Or otherwise just admit that human cognition is too subjective and fuzzy,and

    we are just browsing around hoping to hit on something that seems to work.

    == Chris Glur.