Remove normalization tests for Sort?

dhall-lang / dhall-lang

Maintainable configuration files

https://dhall-lang.org

BSD 3-Clause "New" or "Revised" License

4.22k stars 172 forks source link

Remove normalization tests for Sort? #1106

Open ocharles opened 3 years ago

ocharles commented 3 years ago

My understanding is normalisation is only defined in the context of well-typed expressions, but Sort doesn't have a type, so it's meaningless to ask for its normal form. Due to this, my test suite is currently stuck on dhall-lang/tests/normalization/success/unit/SortA.dhall, and I'm not sure how to proceed.

Nadrieril commented 3 years ago

I just skip it. The test alpha-normalization/success/unit/FunctionNestedBindingXXFreeA.dhall is similar: it's not well-typed but might be useful for an implementation anyways.

Gabriella439 commented 3 years ago

My suggestion is:

Remove the SortA.dhall test

It doesn't add much value, in my opinion
Make the FunctionNestedBindingXXFreeA.dhall type-correct

Nadrieril commented 3 years ago

FunctionNestedBindingXXFreeA.dhall cannot be made type-correct. It's point is to check for the correct handling of free variables, for implementations that support that. dhall-rust used to support that, and this was a very useful test to have.

Gabriella439 commented 3 years ago

Oh yeah, good point. Never mind

ocharles commented 3 years ago

Edit: sorry, ignore this comment. It was about type-inference tests, but this issue is about normalization tests.

ocharles commented 3 years ago

So, just to wrap this one up, am I OK to submit a PR removing SortA.dhall? That at least solves my problem with the beta-equivalence tests.

sjakobi commented 3 years ago

https://github.com/dhall-lang/dhall-lang/blob/master/standard/beta-normalization.md#constants specifies how to normalize Sort. So I think the test is useful for implementations that can handle it.

If it's important to separate the ill-typed test cases, maybe we can keep them separately in normalization/success/ill-typed.

Nadrieril commented 3 years ago

I'd also add that the current type inference rules ensure that the resulting type is normalized. Since Sort is a possible such output, being able to normalize Sort is sensible