Update spec to say that if can return a type

[mheiber]

Description

Before this change, conditional branching based on
types was not allowed for if expressions.

-- Error: ❰if❱ branch is not a term 
let f= \(b : Bool) -> if b == True then Natural else Integer
in 3

But types-that-depend-on-booleans is allowed using a union with merge:

let MyBool = <T | F>
let myIf: MyBool -> Type = \(b: MyBool) ->
        merge
          { T = Bool
          , F = Natural
          }
          b    
in 3

per @Gabriel439 this was "an unintentional inconsistency
in the language due to how it evolved, and the inconsistency can be fixed."

source: https://stackoverflow.com/a/64525640/2482570

related: merged PR allowing record and union alternatives
to be types: #91

Use case

If MyBool is more capable than built-in Boolean people might start defining their own booleans, which will make for some hard-to-follow code. (This might be pretty far-fetched scenario.)

[Nadrieril]

Nicely caught! This is indeed desirable. Could you add some tests to the test suite that check for this situation? Something simple like if True then Bool else Natural would be enough.
And remove dhall-lang/tests/type-inference/failure/unit/IfBranchesNotType.dhall which currently enforces the current behavior.

[Nadrieril]

I think you want Sort as well; that would allow if True then (Type -> Type) else Type, since Type : Kind : Sort. But more generally, do you know what this comment is trying to forbid? I can't find a test case that would trigger this type error. I think we don't actually need it

[philandstuff]

Yeah, I think it’s a theorem that the type of the type of any expression is Type, Kind, Sort, or undefined (eg the type of the type of Kind or Kind -> Kind is undefined).

I guess we should think about that case - what about if x then Kind else Kind -> Kind? I’d be happy to disallow it but I have no strong feeling one way or the other.

[mheiber]

I tried to include new failure and success tests, but have the feeling I may be misunderstanding.

For consistency, I was trying to match the behavior of unions + merge (like in the MyBool example). I was going on the assumption that Boolean and MyBoolean would be pretty similar.

{ a = Kind } errors in dhall-haskell, and it sounds like the standard says it should error as well:

"A non-empty record can store terms, types and kinds" - suggests that a Sort (such as Kind) cannot be stored in a record, which matches the dhall-haskell behavior: { a= Kind } errors

On the other hand, the following seems to suggest (to me) that a Sort can be stored in a record:

"If the type of a field is not Type, Kind, or Sort then that is a type error."

[Nadrieril]

I agree with the reading that { a = Kind } is invalid, because it would need to have type { a : Sort }, which itself does not typecheck. So if we want consistency with merge yeah I agree we want to restrict the kinds of the branches of if.
The way we usually resolve those questions is by asking how it would get desugared into CCω. @Gabriel439 you're the expert on this, any thoughts?

[Gabriella439]

If we were to hypothetically desugar if to a merge expression, then the equivalent type-checking rule would be to type-check the following record of handlers:

{ True = l, False = r }

… which is equivalent to adding the following type-checking rules (in addition to the rules already present):

Γ ⊢ L : c₀
Γ ⊢ R : c₁

In other words, restore the deleted rules, except we no longer enforce that the type of the type of each branch is Type.

As far as the sentence in the standard goes, the way I would phrase it is: "If either branch of the if expression is not a term, type, or kind, then that is a type error." Carefully note that not all expressions are terms, types, or kinds. For example, Kind (while a valid expression in isolation) is neither a term, type or kind, so it would not be a valid branch of an if expression.

There isn't a good terminology for the class of expressions like Kind or Kind → Kind, but I guess we could call them lowercase-'s' sorts and define the term to mean an expression whose type is Sort. However, that definition would exclude an expression like λ(x : Kind) → Kind (although such an expression is a type error, so maybe that's alright).

[Gabriella439]

Here is the matching change to the Haskell implementation: dhall-lang/dhall-haskell#2080

[Gabriella439]

@mheiber: For future reference, you will want to wait longer before merging. 3 votes are required to merge within 3 days, otherwise you need to wait 7 days. For more details, see:

• Contributing to Dhall - How do changes get approved?

However, it's not a big deal and we likely don't need to revert. I doubt any of the other implementations will object to this change.