1. 5

      Wonderful article! It articulates and supports the concept extremely well.

      It’s also very relevant to the programming language I’m designing. It supports the full range of substructural types, with full type inference of required capabilities (using a type class / traits system). This means, for example, that code that does not move values on the stack(s) will not require the “Move” trait, and can thus be trivially compiled to use stack allocation.

      And linear types will be used for I/O, so that all functions remain pure, but you don’t need the complexity of Monads like in Haskell. All such capabilities/effects will be infered and tracked by the type system.

      1. 1

        Neat! Is there a website?

        1. 1

          No, not yet. It will probably be a bit before it’s ready for that, but I do hope to get there as quickly as possible.

        2. 1

          And linear types will be used for I/O, so that all functions remain pure, but you don’t need the complexity of Monads like in Haskell.

          Are you referring an API like this?

          getLine : s -o (s, String)
          putLine : String -> s -o s
          
          main : s -o (s, Int)
          main = ...
          
          1. 1

            It’s a (the first?) multi-stack concatenative language, so you don’t have to explicitly thread linear values through every function call. All functions are inherently linear functions from one state of the (implicit) multi-stack to the next state of the multi-stack.

            The surface syntax will likely be simpler, but the fully explicit type for a “print line” term will be something like:

            (forall s1, s2, w WriteStr . $: s1 * Str $stdout: s2 * w -> $: s1 * Str $stdout: s2 * w )
            

            Where the identifiers between $ and : are the stack identifiers (empty for the default stack), the variable w is qualified by the WriteStr trait, and the stack variables s1 and s2 can expand to any product type.

            The stack variables make the function (multi-)stack polymorphic. If you’re interested in learning more about stack polymorphism, I highly recommend this blog post from Jon Purdy: http://evincarofautumn.blogspot.com/2012/02/why-concatenative-programming-matters.html?m=1

            In order to clone, drop, or move a value, it must possess the Clone, Drop, or Move trait, respectively. In this way, we can support the full range of substructural types, making the type system quite expressive! This makes it possible to express things like a file handle that must be opened before being written to and an open file handle that must be closed before it can be dropped.

            1. 1

              That’s a dense-looking type signature. Let me try to make sense of it:

              So ‘print line’ transitions two stacks - the default stack and a stack called stdout. ‘print line’ expects a Str on top of the default stack, and a WriteStr dictionary on the stdout stack (which I assume contains functions that can actually make a system call to print to stdout). ‘print line’ does not change the default stack or the stdout stack.

              Is that right?


              Purity for applicative languages is something like equivalence between programs f <x> <x> and let y = <x> in f y y for all f and <x> (where <x> is some source code, like 1 + 2 or print("hello")).

              What’s the equivalent in a concatenative, stack-based language? I’d guess an equivalence between programs f <x> <x> and f dup <x>. It doesn’t look like your ‘print line’ has this property. (I might be wrong about what to expect from a pure concatenative language, though.)

              The reason I bring this up is because given what you’ve told me, I don’t think that this is true of your language yet:

              And linear types will be used for I/O, so that all functions remain pure, but you don’t need the complexity of Monads like in Haskell.

              1. 1

                Is that right?

                Essentially, yes. (There’s a minor detail that the WriteStr dictionary is not actually on the stack. Rather a type that implements the WriteStr trait is on the stack. In this case, it’s effectively the same thing, though.)

                Purity for applicative languages is something like equivalence between programs f and let y = in f y y for all f and (where is some source code, like 1 + 2 or print(“hello”)).

                What’s the equivalent in a concatenative, stack-based language?

                Let’s make the example concrete. In Haskell you would have

                f (putStrLn "hello") (putStrLn "hello")
                

                is equivalent to

                let y = putStrLn "hello" in f y y
                

                In this linear concatenative language, you might correspondingly have

                ["hello" putStrLn] ["hello" putStrLn] f
                

                is equivalent to

                ["hello" putStrLn] clone f
                

                Note that terms between brackets are “quoted”. That is, they are pushed onto the stack as an unevaluated function, which can be later evaluated using apply.

                I believe this fulfills the notion of purity you’re describing, unless I’m misunderstanding something.

                Edit: To be clear, cloning is only allowed here because both "hello" and putStrLn, and thus ["hello" putStrLn] implements the Clone trait. If you tried to clone a function that closed over a non-Clone type, then it would not type check.

                Edit 2: And because it might not be clear where linearity comes in, the value on top of the $stdout stack that implements WriteStr is linear. So when you go to evaluate putStrLn, you must thread that value through the calls. Thanks to the multi-stack concatenative semantics, such value threading is completely implicit.

                This has an advantage over Haskell’s monad system in that there’s no need for monad composition and all the associated complexity (which I have a lot of trouble wrapping my head around).

                1. 2

                  I believe this fulfills the notion of purity you’re describing, unless I’m misunderstanding something.

                  That seems right.

                  Thanks for the chat! You’ve given me a lot to think about.