The Privilege of Buda united Hungary and Poland, similarly Buda notation unites Hungarian notation (name variables after their type) with Polish notation (use prefixes of known arity to process things without ambiguity).
Operators: the character '
is reserved for functions, and it accepts two types. Following Joel
Spolsky the first type is
the output and the second type is the input. So 'yx
is a segment of a variable name identifying
a function variable of type x -> y
.
Leading '
characters are inferred at the beginning of the variable name to make the name make sense.
So if you only wish to denote a function x -> y
the proper name is yx
. This behavior can also be
recapitulated inside the name with an _
character, it applies to the entire rest of the name and
inserts '
characters in order to make the rest of the name a well-defined type. (TODO: I think this
makes more sense being the opposite associativity, so that you would write zx_zy_yx
for the function
composition function (x -> y) -> (y -> z) -> (x -> z)
, but I need to explore that more.)
Trailing digits are ignored, they are useful for distinguishing two things of the same type. Internal
digits could also be ignored or could be left undefined for later extensions or something... in
particular they may be convenient to label tuples, 3
being a tuple of three types for example.
I define l
as a character of arity one which converts its argument type to a list type, and f
as
a more general character of arity one which makes reference to a functor or applicative functor. I
similarly reserve m
for monad and p
as an object of arity two for a pair, while x,y,z
and
a,b,c
are reserved as having arity zero, they are always going to by type variables. n
is always
a numeric type variable and i
is always an integer type variable. Pairs do not reverse arguments
the way that functions do.
In the stack machine model we process Buda notation starting from the end of the string. Any arity-N
term pops N arguments off of the stack and then pushes a result onto the stack. Any _
pushes all
remaining terms off of the stack and then pushes one term onto the stack, which will be a function
if the stack had at least two terms on it (otherwise it just leaves the stack the way it was).
So for example we might have a function named lyla''aaa'ypax_lxa
in Buda notation. (This is a bit of
a strange long example but let us go with it. It is processed reverse first by the following steps:
Initial stack []
Received <a>, arity 0, so the stack is: { a } : []
Received <x>, arity 0, so the stack is: { x } : { a } : []
Received <l>, arity 1, so the stack is: { [x] } : { a } : []
Received <_>, arity *, so the stack is: { a -> [x] } : []
Received <x>, arity 0, so the stack is: { x } : { a -> [x] } : []
Received <a>, arity 0, so the stack is: { a } : { x } : { a -> [x] } : []
Received <p>, arity 2, so the stack is: { (a, x) } : { a -> [x] } : []
Received <y>, arity 0, so the stack is: { y } : { (a, x) } : { a -> [x] } : []
Received <'>, arity 2, so the stack is: { (a, x) -> y } : { a -> [x] } : []
Received <a>, arity 0, so the stack is: { a } : { (a, x) -> y } : { a -> [x] } : []
Received <a>, arity 0, so the stack is: { a } : { a } : { (a, x) -> y } : { a -> [x] } : []
Received <a>, arity 0, so the stack is: { a } : { a } : { a } : { (a, x) -> y } : { a -> [x] } : []
Received <'>, arity 2, so the stack is: { a -> a } : { a } : { (a, x) -> y } : { a -> [x] } : []
Received <'>, arity 2, so the stack is: { a -> a -> a } : { (a, x) -> y } : { a -> [x] } : []
Received <a>, arity 0, so the stack is: { a } : { a -> a -> a } : { (a, x) -> y } : { a -> [x] } : []
Received <l>, arity 1, so the stack is: { [a] } : { a -> a -> a } : { (a, x) -> y } : { a -> [x] } : []
Received <y>, arity 0, so the stack is: { y } : { [a] } : { a -> a -> a } : { (a, x) -> y } : { a -> [x] } : []
Received <l>, arity 1, so the stack is: { [y] } : { [a] } : { a -> a -> a } : { (a, x) -> y } : { a -> [x] } : []
Implicitly received another `_` at the end of the expression, so the stack is
{ (a -> [x]) -> ((a, x) -> y) -> (a -> a -> a) -> [a] -> [y] } : []
The resulting function, though it is complicated, could be implemented like so:
flowingSequence :: (a -> [x]) -> ((a, x) -> y) -> (a -> a -> a) -> [a] -> [y]
flowingSequence = lyla''aaa'ypax_lxa where
lyla''aaa'ypax_lxa lxa ypax aaa la = map ypax $ concatMap (lpax_palx . palx_a) la2
where
la2 = scanl1 aaa la
palx_a a = (a, lxa a)
lpax_palx (a, lx) = map pax_x lx
where pax_x x = (a, x)
In some ways this is tongue-in-cheek but in some ways this is very much a serious proposal; having these names does allow for a certain amount of ease in writing the code and perhaps even some ease in understanding it once you pass by the initial difficulty of learning how to read the notation.