Geek Answers Handbook

How to match type for value in Idris / Agda / Coq?

I am trying to define a function called byteWidth that captures the use of the "byte width of a specific atomic type".

My first test:

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

And the Idris compiler complains: "Checking the left side byteWidth: No explicit types on the left side: Int"

My second test:

 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 as byteWidth 'a' , but not byteWidth Char .

+7
dependent-type agda idris coq
source share
2 answers

Your second attempt was really close to a fundamental decision. As you noticed, the problem is that you cannot take type a as an argument when implementing BW a . But you don't care, since you can always explicitly specify an implicit argument.

This gives us:

 interface BW a where byteWidth_ : Int implementation BW Int where byteWidth_ = 8 implementation BW Char where byteWidth_= 1

And you can restore the desired type by partially applying byteWidth_ like this:

 byteWidth : (a : Type) -> BW a => Int byteWidth a = byteWidth_ {a}
+9
source share

In Idris, you cannot map a pattern to a type, and suppose you can, no one is allowed to list all possible types, so it cannot be complete.

The only thing you need is proof that type a is inside some specific set, and we call this sentence 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 automatically generate evidence on the call site, so you can call byteWidth as byteWidth Char instead of byteWidth Char {prf = ChaBWA} .

+1
source share

More articles:


All Articles