Re: [stack] Re: How the Interpreter Works

On Apr 15, 2008, at 2:04 PM, William Tanksley, Jr wrote:

>> So, back to concatenative programming.  Most if not all proofs
>> done in Haskell rely on the type system.  The Haskell type
>> system enforces referential transparency.  Cat is the only stack
>> language I know of that has a type *system* that might be up
>> to the task.  Yet I hear people on this list claiming that the
>> property of concatenativity alone will get you to a place where
>> formal methods become practical.  What about it?
>
> Well, a type system is itself a formal method; it's just a subset of
> more extensive automated proofs. Fifth is another concatenative
> language that, in addition to an inferenced type system, has an
> effects system. I don't know whether its effects system is influenced
> or benefitted by its concatenativity.

The concatenative nature of Fifth *hugely* simplifies things. Let's  
assume for the moment that all of the data structures in Fifth are  
persistent/immutable. The effect system therefore only needs to track  
IO (reading from a file, generating random numbers, etc). We can  
actually add this effect tracking to Fifth without any modifications  
to the type system.

(This probably gets a bit confusing as I wrote this very quickly; skip  
to the end for the summary if you want.)

As has been mentioned here previously, we can conceptualize functions  
that perform IO as reading/writing some "world" value that gets  
threaded through the entire program on the top of the stack. This  
threading is easy to accomplish because of the monoidal nature of  
concatenative language. To be more clear, the 'dup' function normally  
has the following type:

    dup :: R a -> R a a

However, if we were to actually include the "world" in the type, it  
would look like this:

    dup :: R a b -> R a a b

The reason we just use a variable for the world is that 'dup' doesn't  
access it; it just passes it along. However, some functions do modify  
the world. For example, the type of the 'display' function that prints  
a string to the screen would be as such:

    display :: R String a -> R Impure

This type says that display takes some stack 'R' with a 'String' as  
the second element and a world value of any type on top. The display  
function then yields the stack 'R' with an "impure" world on the top.  
In other words, display takes a string and any world and yields a  
string with a modified world.

Now if we look back at the type of 'dup', we can see that composing  
'display' and 'dup' would result in the impure world type being  
propagated forward as 'dup' is simply "a -> a" as far as the world is  
concerned. Essentially, if 'display' is impure, then so is 'display  
dup'.

Finally, we get to the point: If we mandate a world that is "pure",  
then we can enforce that a given function has no side effects. For  
example, here's the full type of 'map' (a simpler type is shown to the  
user):

    map :: R (List a) [R a Pure -> R b Pure] c -> R (List b) c

So what does this say? Well, it's clear that map needs a list. It also  
needs a function. However, the presence of 'Pure' in this function  
says that if given a pure world, the purity of that world must be  
preserved. Accordingly, any function provided to 'map' is guaranteed  
not to have side effects. Note however that 'map' itself can be  
composed in between functions that do have side effects.

Here's one more example of why this system is very nice. The 'o'  
function (called 'compose' in Cat and '.' and Haskell) composes two  
functions on the top of the stack to yield a new function. Including  
the world (again, this is presented more concisely to the user), it  
has the following type:

    o :: R [S a -> T a] [T a -> U a] b -> R [S a -> U a] b

As you can (maybe) see from this type, the manner in which the world  
is handled by the resulting composed function depends on how the two  
functions provided to 'o' handle the world. However, even if these two  
functions have effects and modify the world, this will not make the  
call to 'o' itself impure because its world variable is 'b', not 'a'  
as it is for the functions to be composed.

- - -

I've likely lost you by now, as my explanation isn't very clear, but  
the point is that you get a very useful system that can be used to  
enforce purity -- without the composability headache of monads -- for  
free! If you add another variable to the top of the stack and disallow  
recursive definitions and non-terminating self-application (the  
"occurs check" that prevents infinite types does the latter for you),  
you can track and ensure termination as well!

You might be wondering if you could add yet another variable to track  
mutations to data structures. The answer is that you *can* but the  
results will be too conservative; it becomes impossible to write a  
pure function that is implemented using impure means. To handle this  
properly, we can again do so through adding variables, but these need  
to be attached to the individual parameterized types for the mutable  
values rather than passed on top of the stack. A small addition to the  
type system is then required to handle the enforcement of purity  
properly. However, this is just a 10 line addition to the ~80 line  
type system core type system. (The "non-core" features include  
implicit parameters, aka "globals done right", as well as tracking of  
exceptions.)

- John