Make isNormalized consistent with normalize

[sjakobi]

To be more precise (citing the haddocks):

Given a well-typed expression e, (isNormalized e) is equivalent to
(e == normalize e).

Given an ill-typed expression, isNormalized may return True or False.

An even closer correspondence between isNormalized and 'normalize' is
currently tricky to achieve as 'normalize' returns errors only for some
ill-typed expressions. Once 'normalize' is more principled in this
regard, isNormalized could be changed to return a (Maybe Bool).

This re-enables a property test checking this consistency. Since
'normalize' returns errors for some ill-typed expressions, we
catch have to catch these, which requires an NFData for Expr.

[sjakobi]

Currently the test fails with

      *** Failed! Falsifiable (after 409 tests and 4 shrinks):
      Project ListFold (Left (Set (fromList [""]) (fromList [""])))
      False /= True

There appear to be multiple things wrong with isNormalized here:

dhall-haskell/dhall/src/Dhall/Core.hs

Lines 1938 to 1949 in 81ef514

	Project r xs -> loop r &&
	case r of
	RecordLit kvs ->
	case xs of
	Left s -> not (all (flip Dhall.Map.member kvs) s)
	Right e' ->
	case e' of
	Record kts ->
	loop (Project r (Left (Dhall.Set.fromSet (Dhall.Map.keysSet kts))))
	_ ->
	False
	_ -> not (null xs)

[sjakobi]

Ah, that's an evil one in isNormalized:

      Project r xs -> loop r &&
          case r of
              RecordLit kvs -> ...
              _ -> not (null xs)

Clearly the last line checks whether we're projecting any fields at all, right?

Meeeeep! xs has type Either (Set Text) (Expr s a). not (null xs) is simply isRight xs! The FTP hits again! ;)

[sjakobi]

What should I do about cases like {=}.{ x }?

normalize (since #1071) normalizes this to {=}, ignoring that the field isn't present.

isNormalized follows the standard more closely, checks that the record doesn't contain the field, and returns True.

Of the course the expression didn't typecheck in the first place.

Should normalize be fixed by requiring it to check for the presence of each field?

Can we allow a mismatch between isNormalized and normalize for expressions that don't typecheck?

[Gabriella439]

@sjakobi: They should both behave the same, regardless of whether the expression type-checks. isNormalized is just supposed to be an optimized version of \x -> normalized x == x, so any difference in behavior between the two is a bug

The standard is ambiguous about what the behavior is for an ill-typed expression like this, so any behavior we choose is fine here and we can probably go with whatever behavior is cheaper to compute.

If we really wanted to be pedantic we might interpret the standard to mean that the normal form is {=}.{ x } since there is a normalization judgment of last resort which just normalizes recursively.

[AndrasKovacs]

We should never consider normalization on ill-typed terms. It is highly important to throw internal errors on occasions when normalization encounters ill-typed expressions. Raw terms don't mean anything until checked. This is very strictly enforced in all the compilers out there which support some dependent types (Agda, Idris, Coq, GHC), and should be likewise enforced here, eventually.

It happens that normalization on ill-typed terms is possible right now, but only because of the coincidence of Expr, made possible by the relatively explicit surface language, but it would be better to clearly separate raw syntax and core syntax. There are even some fundamental elaboration performance limitations right now because of the conflation of raw and core syntax. I'll post here a report on NbE normalization tomorrow, maybe I'll expand on this there.

Going back a bit, I prefer that normalization does not silently compute on bad record projections. I doubt that it's performance-critical, but if we want to make it faster, then I am sure that it can be optimized significantly without silently breaking type safety.

[Gabriella439]

@AndrasKovacs: I think that's fine, as long as the two functions behave the same (i.e. if they need to error then they both do so consistently)

[Gabriella439]

Double-check that this comment doesn't get included in the generated haddocks

If it does, then you could move it underneath the Expr type (since that's where people are most likely to insert new constructors anyway)

[sjakobi]

It's not included in the haddocks.

[sjakobi]

I've moved the note anyway.

[Gabriella439]

There's a spoon package which provides utilities for doing this:

hackage.haskell.org/package/spoon/docs/Control-Spoon.html

In this case errorToMaybe is the same as teaspoon

[sjakobi]

Thanks! I made the switch.

I had to use the spoon variant though, as there sometimes were nested errors that weren't caught in WHNF.

[sjakobi]

@AndrasKovacs I agree that it would be desirable that normalizing an ill-typed expression fails, and I hope that NbE gets us there!

We could even have a property test for this!

As long as type-checking and evaluation is separate though, I think it's ok not to repeat the type-checking during normalization.

I look forward to your post! :)

[sjakobi]

@Gabriel439 What do you think about this "contract"?

Otherwise I'd propose returning a Maybe Bool that is Nothing when normalization should fail.

Or maybe a custom type like data Normalized = NormalForm | NonNormalForm | IllTyped or so?

[sjakobi]

I've played around with a Maybe Bool-version of isNormalized a bit. It seems rather tricky to nail down the consistency with normalize though. I think this should wait until normalize itself is more principled, possibly after the NbE changes.

[sjakobi]

I have updated the test to simply discard if normalize returns an error. I'd argue that this covers the cases that we care about the most.

[Gabriella439]

Thank you for restoring that property test! 🙂