See here<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments>and here<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments?from=ReferenceManual.ModellingTypeClassesWithNon-canonicalImplicits>for information about Agda's instance arguments and how they can be used to model type classes.
Also note that implicits (denoted with single braces) are less powerful than instance arguments (denoted with double braces). Also, Agda's "type class instance" search is significantly weaker than Haskell's (here<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Non-recursiveResolutionForInstanceArguments>) because it does not recurse, but I think this is not fundamental but a design choice related to the total functional programming / theorem proving niche that Agda occupies. On Wed, Jul 24, 2013 at 7:21 PM, William ML Leslie < [email protected]> wrote: > 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 > -- Alex R
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
