On Wed, Apr 1, 2015 at 12:38 PM, Matt Oliveri <[email protected]> wrote:
> On Wed, Apr 1, 2015 at 11:40 AM, Keean Schupke <[email protected]> wrote:
>> So:
>>
>> -> = -n->
>> => = -y->
>> +> = -?r->
>
> You mean:
> -> = -?r->
> => = -y->
> +> = -n->
So by my reading Shap and I abandoned thinking about mixed arrow
notation as actually being binary type constructors, even though they
look like they are. The problem is that (int -n-> int) is a weird
type. It's a "function", but you can't call it, because one arg isn't
enough, but it cannot take more than one either. And this type is an
instance of ('a->'b), which seems like a perfectly reasonable type,
except that it might not be. Shap decided that trying to be careful
about how types get instantiated--to avoid things like (int -n->
int)--wouldn't work well, so we now think of function types as being
grouped based on the known call arrows, and a function type whose
final arrow isn't a call arrow is not expressible. This is where afns
come in, because that restriction on the use of mixed arrows
corresponds exactly to what my afn proposal can express.
Shap:
But I thought of a simple-minded alternative. We could just consider
types like (int -n-> int) to be undefined. They have no intro or elim
rules. There's no need to avoid them, but they're basically useless.
Would you prefer binary arrows with silly ones to afn-like grouping?
...
Umm, actually I guess it doesn't matter in the end since programmers
can't write 'n' so inferred/unified types fall in the afn subset. It's
just two ways to formalize it, and the silly types way seems easier.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
