Search code examples
typeclassidris

Is there a value that has a type of Show Int?


According to idris Show Int is a type.

*main> :t Show Int
Show Int : Type

What is of an example of a value that has that type?

*main> :t ?
? : Show Int

What could I replace ? with to get that behavior?

I found the answer to my question here: In Idris, is "Eq a" a type, and can I supply a value for it?


Solution

  • It is this single instance of the Show typeclass

    Show String where
    show cs = strCons '"' (showLitString (cast cs) "\"")
    

    defined in Prelude/Show.idr where the typeclass is also defined