On 4 April 2015 at 08:44, Matt Oliveri <[email protected]> wrote: > > 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. >
I am starting to think it doesn't make any difference anyway. I can adopt the terminology you want for the purposes of clear communication. > 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. > I prefer a logic language for type level expressions, without lambdas. This keeps unification decidable, and keeps unification are the principle implementation method of the type-system (plus backtracking). I think you could replace both unification and backtracking with constraint-resolution, but I don't like the non-deterministic nature of constraint solving (but I could be persuaded to change my mind on that). To avoid repeating the "everything is a type" argument, I will use type-level-object for the rest of this discussion. The logic language only needs atoms, IE type-level objects only need the property of identity (you can generate new type-level-objects, you have type-level-variables (because they can represent any type-level object, not just types), and you have equality (implicit in unification) and inequality. You can introduce type-level booleans and type-level nats for efficiency reasons though, and probably I would want type-level-lists, and type-level-sets to keep type-level-expressions readable. The types inferred from the value-level-expressions become a kind of type-level-object which we can call a Type (because its a kind?). > 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. > Type inference is fine :-) Note the Types are a kind of type-level-object, so the can be an inferable subset of all type-level-objects. (capitalising Types to make it clear its a kind of type-level-object). Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
