[Agda] Recursive instance search limited in depth

[Dmytro Starosud]

Hello Dominique,

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.

Best regards,
Dmytro

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...
>
> Dominique
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda