​Wadler's law aside:​

On 30 March 2015 at 22:17, Keean Schupke <[email protected]> wrote:

> I don't know if this is a difference in terminology or not, but:
>
> On 30 March 2015 at 11:50, Matt Oliveri <[email protected]> wrote:
>
>> On Mon, Mar 30, 2015 at 2:54 AM, Keean Schupke <[email protected]> wrote:
>> > As such the function concretization pass only has to deal with fully
>> > determined arity abstract types.
>>
>> What exactly is fully determined about an arity-abstract type, whose
>> arity is--by definition--not yet determined?
>>
>
> IE we know the whole type:
>
> a -> b -> c
>
> where c cannot be further expanded to (d -> e).
>
> It is fully determined in that we know the number and nature of all
> arguments. A curried function (arity abstract) has no arities to be
> determentd.
>

Making any distinction here whatsoever is breaking parametricity.  There
are three important places where we need to consider concrete types:

* When typing a call expression, the function position must be able to be
given a cfn type in order to emit the correct machine code.

* When typing a call expression, unification of the argument types may make
additional substitutions due to arity constraints.

* When typing a function definition, the function's type must introduce new
variables as necessary to ensure that arity unification is respected by
dataflow.

In neither of these cases is there any useful distinction to be made if the
tail is a function type or not.


-- 
William Leslie

Notice:
Likely much of this email is, by the nature of copyright, covered under
copyright law.  You absolutely MAY reproduce any part of it in accordance
with the copyright law of the nation you are reading this in.  Any attempt
to DENY YOU THOSE RIGHTS would be illegal without prior contractual
agreement.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to