Skip to content

Instantly share code, notes, and snippets.

@crdrost
Created August 1, 2019 16:49
Show Gist options
  • Save crdrost/a19fe0280b7e6e2468521b648819fc6d to your computer and use it in GitHub Desktop.
Save crdrost/a19fe0280b7e6e2468521b648819fc6d to your computer and use it in GitHub Desktop.
Buda notation

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.

Example in the stack machine model

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment