I see. I would say you can't do type-based dispatch with Curry-style
or refinement types. So you're right that qualified types wouldn't be
just tacked-on information.

This is good, this is what I wanted us to figure out: which ways that
BitC uses types ought to be Curry-style. Type-based dispatch isn't one
of them.

(You can make type-based dispatch more Curry-style by explicitly
separating the type metadata for dispatch from the type itself. But I
don't know yet if there's a reason to for BitC.)

On Tue, Jul 22, 2014 at 11:07 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Mon, Jul 21, 2014 at 12:29 PM, Matt Oliveri <[email protected]> wrote:
>>
>> On Mon, Jul 21, 2014 at 12:07 PM, Jonathan S. Shapiro <[email protected]>
>> wrote:
>> > On Sun, Jul 20, 2014 at 11:43 PM, Matt Oliveri <[email protected]>
>> > wrote:
>> >> At any rate, Curry-style
>> >> types are basically just extra tacked-on information about an existing
>> >> thing.
>> >
>> > Until you get to qualified types, I think I agree.
>>
>> You said something like that on another thread too. I looked up
>> qualified types and it seems like a generic way of restricting the
>> domain of type quantification. Semantically, it seems to provide
>> predicates on types. I don't understand why this would change the
>> nature of Curry-style typing.
>
> The issue, in my mind, comes down to implementation. Qualified types
> introduce ad hoc polymorphism that is dispatched on type. If you erase the
> types, then you haven't got anything to dispatch on.
>
> Now that's a quibble, because the type erasure story is a whole-program
> story, and in a whole-program story you get to cross module and lexical
> scope boundaries and rewrite the program before erasing, and then you're
> fine. But you need to rewrite the program (e.g. to make the type class
> instance invocations explicit) before you can erase. So in a certain sense
> you aren't erasing the types from the original program.
>
> More generally, I think that any language that has some form of type-based
> dispatch runs into the same issue.
>
> Is this a conceptually big deal? No. It's just a line in the sand that we
> should take notice of as we stop over it and get on with the job. Mainly
> because some forms of type-based dispatch are more difficult than others for
> our purposes.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to