I was planning to look over Matt's AFN approach today, but there is something he said about the arrow idea I have been developing that doesn't seem right, and it looks to me (at first) as if the afn proposal has the same problem buried in a different place.
First, let me deal with one dangling question. Matt asked at one point whether cfn 'a 'b 'c=>'r 'a-n->'b-n->c-y->'r are the same type. It hadn't occurred to me that this was so, but it seems right. Which is kind of nice, because it means that the rules for combining these "annotated arrow" types are a bit easier to understand. This hadn't been apparent to me before, perhaps because I had never written the 'n' arrows explicitly. OK. On to Matt's concern. In essence, it seems to be that we have two parameters that cannot specialize independently. So when we see: 'a->...->'b-?r->'c we can specialize that '?r' to 'y' only if we know that 'c is not a function type (which therefore might introduce more arrows on the right). I think Matt's objection is that there is a functional dependency here between ?r and 'c, and that it has crept into the type rules. Another way of saying this is that we have a type rule that is partially type-driven rather than purely syntax driven. Something like (warning: unicode characters follow): Γ ⊢ t1 -?r-> t2 Γ ⊢ t2 :: NonFunctionKind ---------------------------------------------------------- t1 -y-> t2 That is: the moment we know the result type is not a function we are allowed to fix the ?r to 'y'. Aside from the fact that I've probably boogered the writing of the rule somehow, the real problem is that it isn't really syntax driven. It's very much like an implicit coercion that way. The problem that this rule introduces is a problem of convergence; we need to confirm that if two type rules modify this arrow, they do so with the same result. I provisionally think that the problem of non-independent type variables applies to afn types as well. When I specialize the argument type variables, I have to update the arity type variable as well. Perhaps Matt can explain to me why that isn't an issue? shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
