Sorry about duplicate mail, I'm on a train with intermittent connectivity. On 1 Apr 2015 08:45, "Matt Oliveri" <[email protected]> wrote: > > On Wed, Apr 1, 2015 at 3:23 AM, Keean Schupke <[email protected]> wrote: > > Hmm but that variable does not follow normal unification rules. Its not a > > type variable, but looks like a kind of expansion variable? > > Right, variables like ?ar are not type variables. We haven't finished > deciding exactly what they are. (We have multiple working options.) > The unification rules might not be too bad, because you never end up > with anything but a plain variable in the surface syntax. But they're > not like unification for HM arrows. > > What is an expansion variable? I found a couple of papers by Sebastien > Carlier, and from one of the abstracts, it doesn't sound like what > we're doing. > > Conceptually ?ar is some type-level information about the concrete > arity an afn has. The only reason an afn is truly arity-abstract is > because its arity parameter is a variable. > > > We agree that arity-aware types break paretricity right? > > I don't see why.
Because they break the smoothness requirement of universally quantified types. choose_one :: a -> a -> Bool -> a The type of 'a' depends on the types unified for each argument. The accepted type is the intersection of the two argument types. Just encoding a single value is not enough. For example: x : a => b c => d y : a => b => c -> d Both would be: cfn 1 a -> b -> c -> d 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. But like you say you then need to wrap arity-abstract types into afns. But then you have to explicitly deal with AFN unification cases. It seems to be turning into a big mess. There is a reason why curried types are used normally. It all seems to be heading towards intersection types to me. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
