On Wed, Apr 1, 2015 at 2:50 AM, Matt Oliveri <[email protected]> wrote:
> On Wed, Apr 1, 2015 at 4:00 AM, Keean Schupke <[email protected]> wrote: > > Both would be: > > > > cfn 1 a -> b -> c -> d > > Whose notation is that? Not ours. > > > You would need at least: > > > > x : cfn [1,2] a -> b -> c -> d > > y : cfn [1,1] a -> b -> c -> d > > > > To deal with this. > > I'm fairly certain you just made this notation up. I figure you're > using deep arities, but we don't use deep arities with cfns. Correct. We don't use deep arities with cfns because there is no need to consider depth, and we don't use shallow arities because all of the arity information we require is present in the type as written: cfn 'a 'b -> 'ret is a concrete function type accepting (exactly) two arguments. If we adopt Matt's list-encoded variable identifying call arrows, I suppose there would be nothing wrong with writing cfn [2] 'a 'b -> ret but note that the [2] is entirely redundant. My personal preference is to avoid this kind of redundancy in types, because it invites user error both in the writing of the types and in the reading of the types. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
