Best way to prevent explosions of complexity

#1

While toying with an idea for a new area to use Dhall, I made a simple Ratio type with associated math functions, and a Haskell program that expects to be provided with functions of type Ratio -> Ratio -> Ratio. This all appears to work when executed, but produces absolutely enormous and slow to compute normal forms when even simple expressions are just passed to dhall.

As an example: a function to compare a ratio with the average of a list of ratios produces an expression which will completely freeze my computer for many minutes before it renders.

The culprit appears to be branches inside the math functions, as I can remove some cases and reduce the size by an order of magnitude or more. The most significant of these being a condition that checks if the denominators of two ratios are equal to avoid multiplying them every time.

Is there a good way to avoid this? I can make the provided functions in Dhall take the record of possible math operations on Ratios as the first argument, but that’s not exactly ideal

#2

@nmerkley: So two three most common contexts for normalizing a function in isolation are:

  • The user requests the normal form

    … which we might be able to improve by providing better ways to browse expressions other than studying their normal form

  • The import resolution machinery pre-normalizes imported expressions

I’m assuming that you’re mostly dealing with the latter case. One idea I’ve been considering is providing some way within the language to configure whether or not an import is α-normalized or β-normalized during the import resolution process (including for imports protected by integrity checks). For example, doing so would also fix this issue:

… since one could specify that imports protected by semantic integrity checks are not α-normalized to retain the original variable names.

This is something that should be pretty easy to standardize, assuming that it addresses the problem that you’re interested in. The hardest part would be deciding on the syntax.