The fancy S meta function accepts an expression as an input and returns a set as an output, where the output set contains all stack identifiers contained in the expression, but not contained within a quote, where a quote is an expression contained in square brackets.
S(i) = {} means that the meta function returns an empty set when applied to an intrinsic. This is so because intrinsics do not contain stack identifiers.
Does that clarify it at all?
No need to apologize! There were no uses of set notation in the previous post, anyways.
Ha, just yesterday I was checking the website to see if there was anything new, then shortly after saw this :)
At first it seemed strange that case_False and case_True are just global names that could be used for other things. Am I understanding right that “stack identifier deshadowing” is what allows you to consider these private in some sense to _False and _True? Also, that reminds me a lot of alpha-renaming in the lambda calculus. Are these essentially the same thing?
The only time a stack identifier can be considered private is when a term doesn’t touch anything that was already on that stack and does not leave any values on the stack. For example, swap can be considered to have two private stacks, because it pushes on to them and then pops off of them exactly what it pushed on.
This becomes more clear when you start writing out the types for terms. The stack-polymorphic type for (s'|(s|swap)) would be something like ∀a b c . <s|a b c -> a c b>. Note that despite pushing and popping off of s1 and s1', neither of those stack identifiers appear in swap’s type. So they can be considered private.
Stack identifier deshadowing might appear to be equivalent to alpha-renaming in the lambda calculus, and there are certainly similarities, but it’s quite different for the following reason: given any valid program, as a user, you can trivially hoist out new terms or inline existing terms without affecting the semantics and without needing to rename any stacks. This is what makes this calculus considerably easier to refactor than the lambda calculus.
I had an interest a few years ago in concatenative languages. I once was interested in how one could transform them into a more traditional representation, because if you could do that you could also provide typechecking for it.
Imagine doing a typed forth where it knows what a certain thing is because it ends up being passed into a certain word that takes some type T.
What do you mean by a more traditional representation? Like into applicative notation? If so, then there’s certainly a way to do that, but the resulting applicative programs would be quite verbose, and ML-based type systems do not support the impredicativity required to properly type check stack-polymorphic higher-order terms. The MLF type system appears to sufficient, though.
Author here. Ask me anything :-)
Realizing I have been out of the game (reading papers like this) for a few too many years…
The meta function fancy-S - what precisely does it mean “set of unquoted stack identifiers contained in e”.
For example why is S(i) = {}?
Sorry if some of this is in the previous post that I don’t have time to read just now.
The fancy S meta function accepts an expression as an input and returns a set as an output, where the output set contains all stack identifiers contained in the expression, but not contained within a quote, where a quote is an expression contained in square brackets.
S(i) = {}means that the meta function returns an empty set when applied to an intrinsic. This is so because intrinsics do not contain stack identifiers.Does that clarify it at all?
No need to apologize! There were no uses of set notation in the previous post, anyways.
Ha, just yesterday I was checking the website to see if there was anything new, then shortly after saw this :)
At first it seemed strange that
case_Falseandcase_Trueare just global names that could be used for other things. Am I understanding right that “stack identifier deshadowing” is what allows you to consider these private in some sense to_Falseand_True? Also, that reminds me a lot of alpha-renaming in the lambda calculus. Are these essentially the same thing?The only time a stack identifier can be considered private is when a term doesn’t touch anything that was already on that stack and does not leave any values on the stack. For example,
swapcan be considered to have two private stacks, because it pushes on to them and then pops off of them exactly what it pushed on.This becomes more clear when you start writing out the types for terms. The stack-polymorphic type for
(s'|(s|swap))would be something like∀a b c . <s|a b c -> a c b>. Note that despite pushing and popping off ofs1ands1', neither of those stack identifiers appear inswap’s type. So they can be considered private.Stack identifier deshadowing might appear to be equivalent to alpha-renaming in the lambda calculus, and there are certainly similarities, but it’s quite different for the following reason: given any valid program, as a user, you can trivially hoist out new terms or inline existing terms without affecting the semantics and without needing to rename any stacks. This is what makes this calculus considerably easier to refactor than the lambda calculus.
I had an interest a few years ago in concatenative languages. I once was interested in how one could transform them into a more traditional representation, because if you could do that you could also provide typechecking for it.
Imagine doing a typed forth where it knows what a certain thing is because it ends up being passed into a certain word that takes some type T.
What do you mean by a more traditional representation? Like into applicative notation? If so, then there’s certainly a way to do that, but the resulting applicative programs would be quite verbose, and ML-based type systems do not support the impredicativity required to properly type check stack-polymorphic higher-order terms. The MLF type system appears to sufficient, though.
Sorry I should have specified. I mean a more traditional language like C or what-not.