[Haskell-cafe] open and closed

[wren ng thornton]

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