Why we cannot pattern match on Set/Type in Coq/Agda/Idris？

Question

Think about a function which accepts a Set, and returns its byte length, named byteLength:

byteLength : Set -> Maybe Nat

and if I want to implement this function directly, I need to pattern match on the type argument:

byteLength Char = Just 1
byteLength Double = Just 8
byteLength _ = Nothing

but the above code doesn't compile since pattern matching on Set/Type is not allowed.

so we have to define an Interface as a workaround

Interface ByteLength a where
    byteLength : Nat

implement ByteLength Char where
    byteLength = 1

and in a more general way, maybe we can use something like TypeRep to do the similar thing and pattern match on TypeRep. but TypeRep is also defined as an Interface.

I think using Interface and using forall is very different, since Interface means "for some types", and forall means "for all types".

I'm wondering Why these DT languages don't support pattern matching on Set/Type, is there some special reason which I don't know?

Answer 1

In Agda, Idris, Haskell, and many other languages quantification over types is parametric (as opposed to ad-hoc polymorphism where you are allowed to match on types). From an implementation point of view, this means the compiler can erase all types from the program, since a functions can never computationally depend on an argument of type Set. Being able to erase types is especially important in dependently typed languages since types can often become huge expressions.

From a more theoretical point of view, parametric polymorphism is nice because it allows us to deduce certain properties of a function by just looking at its type, described eloquently as "free theorems" by Phil Wadler. I could try to give you the gist of the paper, but you should really just go and read it instead.

Of course, sometimes ad-hoc polymorphism is required to implement a function, which is why Haskell and Idris have type classes (Agda has a similar feature called instance arguments, and Coq has canonical structures as well as type classes). For example, in Agda you can define a record like this:

record ByteLength (A : Set) : Set where
  field
    theByteLength : Nat
open ByteLength

byteLength : (A : Set) {{_ : ByteLength A}} -> Nat
byteLength A {{bl}} = bl .theByteLength

and then you can define the byteLength function for various types by defining instances:

instance
  byteLengthChar : ByteLength Char
  byteLengthChar .theByteLength = 1

  byteLengthDouble : ByteLength Double
  byteLengthDouble .theByteLength = 8

With this code, byteLength Char evaluates to 1 and byteLength Double evaluates to 8, while it will raise a type error for any other type.