On Sat, Jul 27, 2013 at 6:08 PM, William ML Leslie <
[email protected]> wrote:
> To show what I'm uncomfortable about, I'll use the signature you
> provided. I /think/ there are five arguments to the sort function,
> several of which are present only for typing. These are:
>
> 0. The element type.
> 1. The Ord instance that will operate on the element type.
> 2. The coercion (~) from the element type to the typeclass.
> 3. The length of the array.
> 4. The array itself.
>
Looking at it in this explicit way, and thinking about Agda's implicit
instance arguments, I wonder about another possible approach..
Has there been any look at causing typeclass-instance selection to be
implicitly lexically scoped in the caller?
Explained by way of mechanism... the declaration and use of the typeclass
including Ord could tell the compiler to implicitly add the trait-instance
as an argument to the function and all functions which call the function to
the module boundary.
This is effectively admitting that one reason we don't explicitly
parameterize the implementation of ord to begin with is the cumbersomeness
of handing the parameter through arbitrary call-stacks to reach it's
intended destination. However, our goal is in fact to offer control of the
Ord implementation to the caller, or we would not have used a polymorphic
mechanism at all.
Agda style implicit instance argument mechanism addresses implicitly
*supplying* this argument during a call. The above suggestion addresses
implicitly *parameterizing* and *propagating* the argument from the
use-site.
-----
I recently came up with this idea as I was thinking about a different but
related problem, which is how to allow explicit allocator selection without
forcing us to (a) write code that explicitly parameterizes the allocator,
and (b) constantly supply the allocator parameterization argument.
My idea was to create a new type of function decorator "context", which
causes *every* use of the function to implicitly parameterize use of that
function. In modules this implicit argument would propagate to the module
boundary. In programs, like Agda implicit arguments, use of the
module-function would implicitly supply the default implementation, unless
an alternative implementation were explicitly specified either at the call
site, or in a program declaration.
In case all that prose was insufficient, here is an example..
// these declarations
context void *malloc(int size);
context void free(void *ptr);
// turn this...
Foo* myfunction() { return malloc(sizeof(Foo)); }
// into this...
Foo* myfunction(myMalloc=malloc) { return myMalloc(sizeof(Foo)); }
// in addition to explicit overriding at the call site, we might allow
bind malloc to MyNewMalloc
bind myfunction:myMalloc to MyNewMalloc
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
