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
.
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}
.
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}
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With