On Sat, Apr 4, 2015 at 4:25 AM, Keean Schupke <[email protected]> wrote: > On 4 April 2015 at 08:44, Matt Oliveri <[email protected]> wrote: >> 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.
OK, so you're a type inference and logic programming fan. Maybe that's why you were talking about Twelf, but didn't know LF. Does your reason for having separate Bool types for each universe have to do with type inference? If so, and if you'd said that, it would have been easier to understand you. I had an argument with Shap before about how much importance should be attached to type inference. The gist of it is that I think first, you want to get an expressive language, and requiring type inference to always work gets in the way. After you know you can express what you want, you can look into sublanguages with tractable, useful inference. I effectively lost the argument, because Shap is convinced BitC can express what he wants, while supporting type inference. But I want to express more. >> 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. Good point. But if we allow the user to write a type outside the subset, it could mess things up, right? So to preserve type inference you'd need to rule it out in some way. > (capitalising Types to make it clear its a kind of type-level-object). I don't mind if we make a special case of "type" when writing in English. As long as we don't use "type" generically to refer to Types and kinds. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
