On 4 April 2015 at 10:38, Matt Oliveri <[email protected]> wrote: > > 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. >
Well, I haven't written much Twelf, but the dualism between dependent-types and logic programs was what interested me. 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 missed out all the type-inference stuff. Its a reason, i'm not sure its the ony reason. > 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. > I generally don't like type-annotations. I like Mark Jones's FCP where you don't need to annotate higher order functions, but constructors have special intro/elim rules, and I haven't really fully thought through the consequences of adopting this. What I do want are type constraint annotations, so you can take the inferred type and constrain it with axioms added in the logic language at the type-level. > > 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. > If Types are an inferable subset of type-level-objects, you could write any type and it should not mess up type-inference. If you wrote a type-level-expression that was not a Type, it would not be a valid type! It would be a type level expression. With type-level logic programming, we would say the type-level program needs to evaluate to true in order for the program to compile, else it would return an error. Much like a type-level assertion. Such expressions could be made of Type kinds and non-Type kinds, but types must be Types. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
