How to write and align type inference rules?

[Marvin]

Hi! I started learning Typst yesterday and I’m currently in the process of translating some LaTeX code to Typst and was wondering how I can elegantly (and typographically beautiful) write type inference (i.e. natural deduction, gentzen, sequent calculus) diagrams.

In LaTeX I use

\begin{mathpar}
    \inferrule*[right=Var]
    {x : \tau \in \Gamma}
    {\Gamma \vdash x : \tau}

    \inferrule*[right=Abs]
    {\Gamma, x : \tau_1 \vdash e : \tau_2}
    {\Gamma \vdash \lambda x : \tau_1.\ e : \tau_1 \to \tau_2}

    \inferrule*[right=App]
    {\Gamma \vdash e_1 : \tau_1 \to \tau_2 \\
     \Gamma \vdash e_2 : \tau_1}
    {\Gamma \vdash e_1\ e_2 : \tau_2}
\end{mathpar}

Which results in the following:

In Typst the only thing I could come up with is using stacks (or grids) to manually align curryst prooftrees (which is a bit overkill for these diagrams I think):

#align(center, stack(dir: ttb, spacing: 2em, stack(dir: ltr, spacing: 15%,
  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$
    )
  )
))

I particularly don’t like how I have to manually adjust the spacing (compared to mathpar), especially if I had a lot more than three diagrams.

Is there any better way to do this? Is there something similar “magical” to mathpar in Typst?

[Eric]

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$
    )
  ),
)

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!)

[SillyFreak]

Hi @Marvin, could you maybe try to revise your post’s title to be a complete question as per the question guidelines:

Good titles are questions you would ask your friend about Typst.

We hope by adhering to this, we make the information in this forum easy to find in the future. Thanks!