How to write and align type inference rules?

Questions
,
2

There is no inbuilt mathpar alternative, but it is possible to write something similar yourself, as I have done with the following code:

#let mathpar(
  numbering: auto,
  row-gutter: 1.2em, // can be set to 'auto'
  column-gutter: 2.5em,
  ..children
) = layout(bounds => {
  // Resolve parameters
  let numbering = if numbering == auto { math.equation.numbering } else { numbering }
  let row-gutter = if row-gutter == auto { par.leading } else { row-gutter.to-absolute() }
  let column-gutter = column-gutter.to-absolute()
  let children = children.pos().map(child => [#child])

  // Spread children into lines
  let widths = children.map(child => measure(child).width)
  let lines = ((children: (), remaining: bounds.width),)
  for (child, width) in children.zip(widths) {
    if (
      child.func() == linebreak or
      (lines.last().remaining - width) / (lines.last().children.len() + 2) < column-gutter
    ){
      lines.push((children: (), remaining: bounds.width))
    }

    if child.func() != linebreak {
      lines.last().children.push(child)
      lines.last().remaining -= width
    }
  }

  // Layout children in math mode for baseline alignment
  par(leading: row-gutter, math.equation(numbering: numbering, block: true,
    for (i, line) in lines.enumerate() {
      let space = h(line.remaining / (line.children.len() + 1))
      par(leading: par.leading, space + line.children.join(space) + space)
      if i != lines.len() - 1 { linebreak() }
    }
  ))
})

It is by no means perfect, but when used with your example, it certainly does the job. You can use it like this:

// This is necessary, because the default math font does not
// support small capitals, so we have to explicitly switch
// back to the text font here.
#show smallcaps: set text(font: "Libertinus Serif")

#mathpar(
  proof-tree(
    rule(
      name: smallcaps("Var"),
      $Gamma tack x : tau$,
      $x : tau in Gamma$
    )
  ),
  proof-tree(
    rule(
      name: smallcaps("Abs"),
      $Gamma tack lambda x : tau_1.e : tau_1 arrow tau_2$,
      $Gamma, x : tau_1 tack e : tau_2$
    )
  ),
  proof-tree(
    rule(
      name: smallcaps("App"),
      $Gamma tack e_1 " " e_2 : tau_2$,
      $Gamma tack e_1 : tau_1 arrow tau_2$,
      $Gamma tack e_2 : tau_1$
    )
  ),
)

Output of above Code

You can of course play around with the parameters to improve the spacing. When row-gutter is set to auto, it will use whatever value is used in par.spacing, which defaults to 0.65em. A larger value looks better here though, as there are fractions involved, which like to get close to each other.

(I might have overcomplicated this a bit, so if someone has a simpler solution, please share!)

2 Likes