On 2 April 2015 at 09:17, Matt Oliveri <[email protected]> wrote: > On Thu, Apr 2, 2015 at 4:02 AM, Keean Schupke <[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'. Which is how I was originally proposing to handle this. Universe 1 Universe 0 _Bool True False _Type Int Float Bool etc... Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
