On 24 July 2013 22:59, Alex Rozenshteyn <[email protected]> wrote:
> This reminds me a bit of how Agda encodes type classes using instance
> arguments: if there's exactly one term of the required type in scope at the
> use, it's taken as the argument; otherwise, there is a compile error.
I wasn't aware that Agda had type classes, but if it does, I agree and
find your description simpler. Here's why.
The Vec constructor
_::_ : a -> Vec a k -> Vec a (suc k)
takes two arguments, the item and the tail, and returns itself.
Except that it doesn't really, because that would leave the 'a and the
k unbound, so the full constructor signature is probably more like
_::_ : {level, k : Nat} -> (a : Set level) -> (Vec a k) -> Vec a (suc k)
since the level and the length are actually unused by the constructor
except for type checking, they have no representation at run-time,
nevertheless they must have a value, which is inferred by the usage of
the constructor. The explicit arguments imply a choice of the level
and the length, but if they didn't, you could say `( _::_ ) {k=7} item
rest` or so.
If you apply that to type classes, you might say that a choice of an
instance is implied, not just by the existing arguments, but by there
being exactly one type-correct solution in the scope of the call.
Unlike the implicit arguments in the Vec constructor, instance
arguments do have some run-time impact, but since their value is
usually constant, the function may be partially evaluated against the
instance and methods copy-propagated as needed.
I think this feels simpler for the same reason that writing Agda feels
simpler than writing tactics - we might call them implicit, hidden
arguments, but we know exactly where they come from: they are obvious
from the arguments at the call site.
--
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
