[Haskell-cafe] open and closed
illissius at gmail.com
Tue Aug 31 05:57:49 EDT 2010
On Mon, Aug 30, 2010 at 1:23 PM, wren ng thornton <wren at freegeek.org> wrote:
> 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.
Hmm, I see. I think what had me confused was that type classes seem to
be at the same level as types, and, like functions, to interact with
things at their own level; but then they also interact with something
from one level lower (instance dictionaries), which is why it doesn't
make sense to transplant them to the lowest level (values). Thanks for
> Live well,
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
Work is punishment for failing to procrastinate effectively.
More information about the Haskell-Cafe