On Sat, Apr 4, 2015 at 2:17 AM, Keean Schupke <[email protected]> wrote: > > On 4 Apr 2015 04:53, "Geoffrey Irving" <[email protected]> wrote: >> Yes. In my luddite set theory intuition: "type-level" is a fancy sounding >> synonym for compile time, and "type" is a compile time set of values. A >> specific boolean or natural is not a set of values, except in some pedantic >> set-theory-bootstrapping sense which doesn't matter. > > I tend to agree with this view. If I call all type level objects 'types', > does it break any results you rely on? No, I don't think so.
Yes, well just 'cause it doesn't actually break anything isn't a reason to do it. I know you think there's a reason, but you seem incapable of communicating it to me. > What does matter is distinguishing values which are part of the program, > (hence may not be known about until runtime, and without partial evaluation > we can't know anything about them except maybe constants, and even then if > the constant requires construction we may not know about it until runtime) > and values which are part of the compiler (hence may be evaluated at compile > time and be part of the type system). This is true, and it is important that type-level elements are known before runtime, but I don't think that's the main reason to distinguish bools and Bools, for example. BitC is an imperative language, but type expressions should not have side effects. So we can't allow any bool expression in a type, because it might have a side effect. Also, an arbitrary bool expression might not actually return a bool value, and any type that was depending on that bool is now not a meaningful type. Basically type expressions _want_ to be written in a total, pure functional programming language, which BitC is not. The type level is a cleaner, simpler sublanguage. Speaking of simpler, even total, pure, functional computations can screw up type inference. If you want type inference, your types had better be _really_ simple. So trying to allow bool and Bool to be the same is a huge can of worms. > If we could agree to distinguish these and name them differently then > although we would be using different terminology our systems would at least > be compatible. Perhaps: > > value-level-value > type-level-value > > Would work? I like "value" and "type-level object". But usually we can just refer to a specific type of value or kind of object. The BitC convention seems to be that types are not capitalized, and kinds are, so we know when a kind was written, if we all follow the convention. For example, every Bool is a type-level object, because Bool is a kind, because I used it like a type, except it's capitalized. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
