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

10
votes

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.

2
coqagdaidrisdependent-type

2 Answers

10
votes

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}
2
votes

In Idris, you can not pattern match a type, and suppose you can, it's not possible for anybody to enumerate all possible types, so it can't be total.

The only extra thing you need is a proof about the type a is inside some specific set, and we name this proposition as ByteWidthAvailable.

data ByteWidthAvailable : Type -> Type where
  IntBWA : ByteWidthAvailable Int
  ChaBWA : ByteWidthAvailable Char

total
byteWidth : (a : Type) -> {auto prf: ByteWidthAvailable a} -> Int
byteWidth _ {prf = IntBWA} = 8
byteWidth _ {prf = ChaBWA} = 1

The only trick here is the auto command provided by Idris, which helps to generate a proof automaticly at call-site, so that you can call byteWidth like byteWidth Char instead of byteWidth Char {prf = ChaBWA}.