On 28 July 2013 14:13, David Jeske <[email protected]> wrote:
> 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.
So, you say, "f takes a List of Ord", and the caller says "here is my
List of T, and if you take a look around I think you'll find that T
has an Ord instance".
That's what I was hoping to get at, yes. In some of the examples I've
elided arguments (well, argument definitions) that could reasonably be
inferred, such as the actual element type, or the length of the array.
I declared the instance arguments in two cases because I actually use
them in the body, or provide them explicitly as arguments. And even
if you've had to declare an argument in the function type definition,
it may still be inferred at the caller. So I say
arraySum xs
and the compiler, knowing the type of arraySum, infers the additional
arguments, expanding the call into
arraySum {X} {{my_arith}} {len_xs} xs
and then having to decide what X, my_arith, and len_xs are. my_arith
is the only one that is not /obvious/ from the type of xs, and I
intentionally didn't discuss how to choose the instance argument. So
that's about what I think on the subject, and how I understood what
you were talking about.
This seems to be how Agda/Idris work in general, straghtforward
pattern matching that does the heavy-lifting for you.
> 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.
It's not even a matter of control, by the time we have a type variable
rather than a real type, we have no way to show that an Ord instance
even /exists/. So, the Ord instance needs to be passed around as a
witness from the moment we cast to the typeclass (that is, when we
`forget` the real type of the value).
> -----
>
> 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.
I think this is a bit like passing around region variables as arguments.
--
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
