[bitc-dev] Instance coherence: the shape of a solution

Geoffrey Irving irving at naml.us
Mon Apr 16 13:25:40 PDT 2012

On Mon, Apr 16, 2012 at 1:16 PM, Jonathan S. Shapiro <shap at eros-os.org> wrote:
> On Mon, Apr 16, 2012 at 11:42 AM, Geoffrey Irving <irving at naml.us> wrote:
>> In a functional language
>> it'd be nice to avoid polluting the type system with this distinction
>> between function objects and functions.
> Why? These things have the same type only because their types are
> underspecified w.r.t. "constness".
> If you said: the type system should preserve the ability to treat these
> interchangeably where their compile-time constant-ness is not an issue, then
> I wholly agree. That doesn't mean that they need to have the same type.

I completely agree that their types are actually, fundamentally
different.  However, the result is that the type of map has to become
something like

    map :: f -> List x -> List (f x)

instead of

    map :: (x -> y) -> List x -> List y

The same applies to every single higher order function where you might
want enforced partial specialization.  On the other hand, this does
reflect the actual situation, so I agree that the solution is clear if
we follow the principles out.  I suppose the nonstandard map type is
even shorter than the normal one.

>> In the case of sort, the advantage of passing in a function object
>> instead of a closure transparent to the caller is that it allows the
>> sort function to be partially evaluated without inlining it (if it's
>> inlined everything is easy even with closures).  Is it feasible to
>> hint to the compiler that we want certain things partially evaluated
>> without polluting the type system?
> Why is this polluting the type system? Where should this distinction be
> expressed, if not in the type system?

I happily withdraw my concern, and agree that types are the correct
place for them to go.


More information about the bitc-dev mailing list