On Wed, Feb 18, 2015 at 3:36 PM, William ML Leslie <
[email protected]> wrote:
>
> Thanks Matt, PKE, and Shap.
>
> These two paragraphs are the missing piece of the puzzle. I could write
> it in Idris like so:
>
> > choose_one : {N : nativeFunctionTypeFor (Nat -> Nat -> Nat)} -> N -> N
> -> Bool -> N
>
> stating the variable in the type.
>
If I'm understanding the notation, this is very similar to the one I wrote
a few minutes ago that used a unification constraint. In this notation, the
unification constraint is being written inline.
> ... well, maybe. You also said this, Shap:
>
> choose_one returns one of its arguments; and perhaps x has a curried
>>> definition and y takes two arguments directly. They have the same type, of
>>> course, so this is a perfectly reasonable thing to do.
>>>
>>
>> This is incorrect, because that is *not* a reasonable thing to do. They
>> have the same type. Therefore they are required to have the same concrete
>> type, therefore the same arity.
>>
>>
>
> If there is one concrete type per abstract function type, there's no need
> for quantification at all I guess. Just a global dictionary?
>
I think I answered this a few minutes ago, but it might be worth a brief
digression on *why* I wrote what I did. Perhaps you folks can help me clean
up my lexicon on this.
In my mind, two abstract types that may concretize differently are not the
same type. It may turn out that they are, or it may turn out that they are
not. This is probably because my mental ability to process abstraction is
compromised. :-) I'm not quite sure how I should have written this more
correctly above. Perhaps "identically the same type", but that seems like a
somewhat odd way to say things.
BTW I wrote my email after reading your concrete proposal, but like I said,
> it only talks about applications and parameters and doesn't really deal
> with return values (or case expressions or any other kind of meet). Say,
> you said that paramaters and return values could be abstract, and then only
> talked about inference rules for parameters.
>
I'll respond to this separately.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
