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. 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). 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? Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
