Added `normalizeWith` function.

[aleator]

Added normalizeWith function to complement typeWith.
Dhall is so very attractive base for simple DSLs that I felt it
needed to be pushed over the edge.

Naturally, using normalizeWith loses all the nice features of Dhall.
If your context isn't total or strongly normalizing then embedding it
to Dhall will not improve things.

I didn't spend too much time testing the change since I have some doubts whether this is an acceptable regarding the original mission of Dhall.

[Gabriel439]

I think this is a great idea, but I would suggest a different approach, which is to change the type of normalizeWith to CtxFun a -> Expr s a -> Expr t a, and you apply the CtxFun at the top-level instead of in the App case, like this:

normalizeWith :: CtxFun a -> Expr s a -> Expr t a
normalizeWith (CtxFun f) e = case f e of
    ...

normalize = normalizeWith (CtxFun id)

The reason why is that you might want to implement functions that cannot be normalized until they are fully saturated. An example of such a function in Dhall is List/head: the first argument is the type to specialize to, and that's not enough to begin the normalization process

The other reason I suggest this change is that I expect this to be more efficient. Doing a Map lookup on every App will decrease the performance of the standard normalize function, whereas applying id at the top-level is cheap and the compiler will just inline that away.

[aleator]

I've experimented a little bit with applying CtxFun on the top level. If I understood correctly, there is a slight difficulty (or a decision point) here. On the top level, the argument part of the app is still wrapped in bunch of Notes, making it more tricky to actually write the CtxFuns.

Any opinions how this should be handled? Just (shift 0 .) the CtxFuns before use?

[Gabriel439]

Yeah, that would work. It might also be simpler and more efficient to shift 0 the entire expression just once before beginning recursion, like this:

normalizeWith (CtxFun f) e0 = loop (shift 0 e0)
  where
    loop e = case f e of
        ...

[Gabriel439]

Looks great! Just a few minor suggestions

[Gabriel439]

Looks great! Just a few minor suggestions

[Gabriel439]

Perhaps expand loop here to normalizeWith.loop

[aleator]

Ah. Of course.

[Gabriel439]

Perhaps inline the CtxFun type synonym into the type of normalizeWith since it's only used once

[aleator]

I left this alone, since it saved some typing when writing tests.

[Gabriel439]

In that case, maybe rename it to something like Normalizer since it no longer is part of a context any longer

[Gabriel439]

Parentheses are not necessary around the id

[aleator]

Fixed. I also applied this to other places where search/replace has ended up with extra parentheses.

[aleator]

Here is a new version of this. However, I hit a snag when trying to write tests. Should there be isNormalized that corresponds with normalizeWith, since it now also may depend on the context of normalization?

[Gabriel439]

Yeah, you would need an isNormalizedWith function

[aleator]

I've now moved the application of CtxFun back to App-case from the top level. The previous attempt at this didn't work out, since the normalization was cut short. Also, having all of the ast available to CtxFun seems like an overkill ("Hey, lets go and replace all True's with 42's"). When it is applied as the last case of App you know that it won't be likely to mess up pre-existing stuff that is outside of the captured App.

There are also two tests, which demonstrate how this works.

[Gabriel439]

This seems fine. My only remaining suggestion is to change the type of the function back to forall a . Expr s a -> Expr s a, and change the logic to:

_ ->  ctx (App f' a')

... and then normalizeWith becomes:

normalize = normalizeWith id

... for the same reason as before: efficiency

[Gabriel439]

Minor suggestion: you can use code to input these types:

minType        <- code "Natural → Natural → Natural"
fiveorlessType <- code "Natural → Natural"
wurbleType     <- code "Natural → Integer
let tyCtx = insert "min"        minType
          . insert "fiveorless" fiveorlessType
          . insert "wurble"     wurbleType
          $ empty

I don't feel very strongly about this suggestion, so feel free to ignore me :)

[aleator]

Looks better that way. Will do.

[Gabriel439]

I still suggest naming this something like Normalizer instead of CtxFun since it no longer uses a context

[aleator]

Sorry. I missed your original comment. Will do!

[aleator]

I don't think _ -> ctx (App f' a') would work. Suppose that we have a custom App (matching, say, App (Var "foo") (NaturalLit x)) sitting at the top level, and we hit this case. Then ctx turns this into (App (Var "bar") (NaturalLit x) and the normalizer terminates.

What if the ctx contains a definition for (App (Var "bar") (NaturalLit x) as well?

We also can't loop here without looping forever. We need to know if ctx actually did something before continuing.

The other alternative is to require that all custom primitives produce their results in normal form but this is somewhat more limited approach.

I can probably whip up a criterion for testing how much this slows things down if you are really worried. Can you think of a good test case? (Normalize the prelude? The tutorial?).

[Gabriel439]

Oh yeah, I hadn't though about the need to continue looping. Then I think it's fine as is

I think the performance impact will probably be minimal since it only affects the case where normalization is blocked, which is not that common and not on the critical path