On Thu, Apr 2, 2015 at 4:26 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 09:17, Matt Oliveri <[email protected]> wrote: >> In other words, the ternary "arrow" constructor from your earlier >> email should have the kind: >> arrow :: Bool->Type->Type->Type > > Lets ignore recursive types (they lead to unsound results for a Herbrand > universe). > > A 'kind' seems to me to be a PL term that is not actually part of > intuitionistic logic / type theory, that is equivalent to 'universe 1'.
Something like that, yeah. > Which is how I was originally proposing to handle this. > > Universe 1 Universe 0 > _Bool True False > _Type Int Float Bool etc... OK, I see what you're saying, and this is acceptable. To be pedantic, a universe is a type, so the left half of that table is OK; it says _Bool and _Type are elements of Universe1. But Int, Float, Bool... are elements of _Type; there is nothing actually called Universe0. True and False are elements of _Bool, I assume. They are not types; _Type is a universe, but _Bool is not. When I wrote Bool and Type above, I meant what you are calling _Bool and _Type. I maintain that for the sake of predicativity, there's no need to distinguish _Bool from Bool. (That is, the Bool kind from the bool type.) However, we want to distinguish them anyway to avoid dependent types. So getting back to the original problem, do we now agree that Bool kind is predicative? And that it makes sense for the y/n on an arrow to be of that kind? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
