[Agda] Recursive instance search limited in depth
d.starosud at gmail.com
Wed Oct 2 18:40:05 CEST 2013
Approach I proposed is really powerful (not just because it is
mine:)). Using it I implemented function for determining type
representation for functions on sets and Haskell-like TypeRep (please
see here https://github.com/dima-starosud/Dynamic/blob/master/Test.agda).
Also now I am working on decidable type representation. So it is
definitely more powerful then basic Haskell's type classes.
Also I just came up with an idea how to avoid non termination:
Instance type should be parametrized by Nat or so. And one can define
how deep search should be.
Looking forward to feedbacks.
2013/10/2 Dominique Devriese <dominique.devriese at cs.kuleuven.be>:
> 2013/10/2 Dominique Devriese <dominique.devriese at cs.kuleuven.be>:
>> Non-linear parametric instances
>> could probably be easily abused to decide equality of types, which I
>> think we want to avoid.
> On second thought, this point might be moot. If I remember correctly,
> there is a discussion of tricks for (semi-)deciding type equality
> using type class instances in the HList paper, but I should re-check
> what features they require precisely...
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda