[Haskell-cafe] open and closed

[Gábor Lehel]

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
the explanation!


>
> --
> Live well,
> ~wren
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Work is punishment for failing to procrastinate effectively.