Search for instances given a type

[LeifW]

Currently, :doc Foo where Foo is a class gives you (among other things) the instances (in scope) of that class, e.g.

Instances:
    Functor List
    Functor (Vect n)
    Functor Stream
    Functor PrimIO
    Functor IO
    Functor Maybe
    Functor (Either e)

Based on a twitter convo, an idea by @pminten https://twitter.com/pdxleif/status/466695226937987072, the reverse of that might be useful? That is, given one of those types / expressions, list what typeclass instances exist for that.

So, supplying List could yield: Functor, Applicative, Monad, Foldable, Traversable, Semigroup, Monoid, ...

[david-christiansen]

This should also find instances for things that aren't types :-)

[paulkoerbitz]

If I understand correctly then you guys are suggesting something along the lines of

Idris> :doc List Data type List : Type -> Type Linked lists

Constructors: Nil : List a The empty list

:: : a -> List a -> List a
    Cons cell
    infixr 7

Typeclass instances: Functor List Applicative List ....

Sounds like a great idea.

I'm afraid I don't really understand your comment David. Can a (non-type) term have a typeclass instance?

On Thu, May 15, 2014 at 12:02 AM, David Christiansen < notifications@github.com> wrote:

This should also find instances for things that aren't types :-)

— Reply to this email directly or view it on GitHubhttps://github.com/idris-lang/Idris-dev/issues/1230#issuecomment-43143691 .

[david-christiansen]

Sounds like a great idea.

I think so too!

I'm afraid I don't really understand your comment David. Can a (non-type) term have a typeclass instance?

Yes!

[paulkoerbitz]

David, do you mind giving an example for this? I can't really think of anything...

[david-christiansen]

No time to write real code tonight, but think of something like

class Finite (a : Type) (n : Nat) where
  isFinite : Iso a (Fin n)

instance Finite Bool 2 where
  isFinite = MkIso ...

[david-christiansen]

Fun exercise: implement natural number addition in the type class resolution mechanism :-)

[LeifW]

I also chirped an example class defined for operators in response to his question:

class Commutative a ( op : a -> a -> a ) where
  proofCommutative : ( l, r : a) -> op l r = op r l

instance Commutative Nat plus where
  proofCommutative = plusCommutative

https://twitter.com/pdxleif/status/466626380260597760

[david-christiansen]

@paulkoerbitz Does this stuff make sense now?