How to map Type to Value in Idris/Agda/Coq?

Question

I'm trying to define a function named byteWidth, which captures the usage about "get byte width of specific atomic type".

---

My 1st trial:

byteWidth : Type -> Int
byteWidth Int = 8
byteWidth Char = 1

And the Idris compiler complains: "When checking left hand side of byteWidth: No explicit types on left hand side: Int"

---

My 2nd trial:

interface BW a where
  byteWidth : a -> Int

implementation BW Int where
  byteWidth _ = 8

implementation BW Char where
  byteWidth _ = 1

And in this case, I can only use byteWidth like byteWidth 'a' but not byteWidth Char.

Answer 1

Your second attempt was really close to the principled solution. As you've observed the problem is that you can't take the type a as an argument when implementing BW a. But you don't care as you can always set an implicit argument explicitly later on.

This gives us:

interface BW a where
  byteWidth_ : Int

implementation BW Int where
  byteWidth_ = 8

implementation BW Char where
  byteWidth_= 1

And you can then recover the type you wanted by partially applying byteWidth_ like so:

byteWidth : (a : Type) -> BW a => Int
byteWidth a = byteWidth_ {a}