On 8/29/10 1:33 PM, Gábor Lehel wrote:
Another thing I'm wondering about is that there's a fairly intuitive correspondence between functions at the value level vs. functions at the type level, and datatypes to classify the value level vs. datakinds to classify the type level, but what corresponds to type classes at the value level?
Wouldn't you go the other way: kind classes? Type classes are predicates on types, and the application of a class to a type forms a proposition which represents the type of proofs that the proposition holds (i.e., the type of instance dictionaries). This can be easily extended upwards by having predicates on kinds yielding propositions that represent the kinds of (type-level) proofs. IIRC, this is the perspective that Omega takes. To extend it downward we'd have to ask what it would mean to have a predicate on values. The value-level propositions formed by applying those predicates couldn't have proofs (because there is no sub-value level), so it's not entirely clear what that would mean. If anything, the value-level correspondent of type classes are just uninterpreted predicates, i.e. data constructors. Whether this line of thinking is sensible or just a fallacious attempt to unify everything, I can't say off hand. I think it's better to think of contexts as the type of the invisible lambda for passing dictionaries, just as forall is the type of (the invisible) big-lambda, and -> is the type of lambda. Thus, the dictionaries are the concrete thing you want to generalize to higher levels; the classes will be at the next level up. -- Live well, ~wren