On Mon, Mar 2, 2015 at 2:40 PM, Matt Oliveri <[email protected]> wrote:

> On Mon, Mar 2, 2015 at 11:01 AM, Jonathan S. Shapiro <[email protected]>
> wrote:
> > Aside:
>
> I hope you don't mind if I reply to this, which risks turning into a
> main branch of the discussion.
>

Actually, Matt, I *do* mind. I was very clear here that even I had problems
with my explanation. It was an explicit acknowledgement that I was engaged
in a non-productive and likely wrong set of assumptions and notions.

I do not understand why your frustration meter is set to 20 on a scale of
10 this morning, but I'm not the enemy. It seems to be a pattern that when
you get frustrated with a discussion you become more confrontational. We
all make that mistake once in a while. It's not the end of the world. But
please take a step back, take a deep breath, and calm down a little. Your
contributions here are tremendously valuable, but they *never* arise from
your moments of frustration, because those moments don't lead to effective
communication.



> > Only after
> > the types unify will we learn the return type of f and be able talk about
> > the next specialization step.
>
> But this is only true in the seemingly-irrelevant sense of the
> concrete function's return type. No matter how many concrete
> applications (f a b c) turns into, the return type we care about is
> simply the type of that expression. We can talk about that right away,
> if only via a type variable. Indeed, that type variable may be
> instantiated to a function type, and have its own arity concretize
> before f's arity does. Or at least it seems like an unnecessary and
> yucky proof obligation to assume otherwise. This is the sense in which
> instantiation is not guaranteed to proceed from left to right.
>

Yes, Matt. And this problem is exactly what I was acknowledging when I
wrote that the unifications happen logically in parallel. The whole point
of my email was explaining that I had my head on backwards.


> Also, I should point out that if you allow regrouping, then of course
> this whole explanation is completely screwed.
>

Can you please explain what you mean by "regroup"?


>
> > No new proposition or conclusion here. Just an explanation of why I keep
> > getting stuck in this way.
>
> Shap, for all I know, in your proposal, you _should_ be getting stuck
> that way. That's how confused you've gotten me.
>

I believe that is substantially what I said. Applying a mallet and a chisel
to my head to ensure that I noticed may not have been necessary.


shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to