3 ms·
I have to admit that I am out of my field, so help me a bit, you expressed that it must be dependently typed because false and true are a -> b -> a|b under unio
by PartiallyTyped 3y ago
I have to admit that I am out of my field, so help me a bit, you expressed that it must be dependently typed because false and true are a -> b -> a|b under union (and a->b->b and a->b->a respectively) so the the abstractions can take any functions subtyping a->b->a|b, thus to make them correct you need dependent types to verify that the abstractions take only True and False?
Is this correct?
- cvoss 3y agoThe only types available to you in this flavor of STLC are bool, bool -> bool, bool -> bool -> bool, (bool -> bool) -> bool, etc. Structurally, if `true := \x\y.x`, the simplest attempt at typing it would be `true : bool -> bool -> bool`. But that means `true` can't have type `bool`! What you need is to say that true (like false) chooses one of its two inputs to return, no matter what type that happens to be. So we introduce a type parameter (think Java generics, if that's what you're familiar with). "Given any type T, `true T` has type T -> T -> T". A formalized notation for this (there is more than one notation you'll see) is `true : ∀ (T : Type), T -> T -> T`. And `false` has the same type. This type obviates the need for a declared `bool` type.