Why cannot define function of type 'Set -> Set' in Agda?

Question

Assume there are four types , D, Q, P, C

data Q : Set where
  q1 : Q
  q2 : Q

data P : Set where
  p1 : P
  p2 : P

data C : Set where
  c1 : C
  c2 : C

data D : Set where 
  d1 : D 
  d2 : D

When trying to define function

f : Set -> Set
f D = Q
f P = C

I get the warning unreachable clause .

I assume it is because domains of Agda function are defined on sets but not category of sets. What if I want a mapping relation which behaves like a close type family in Haskell ?

Answer 1

Because the Agda compiler erases types during compilation, it is not allowed to pattern match on Set directly. (The error 'unreachable clause' is a bit confusing but it results from Agda interpreting D as a pattern variable rather than the datatype.)

The usual way to work around this problem is to define your own universe, i.e. a datatype whose elements are interpreted as specific sets. Here is an example:

data Q : Set where
  q1 : Q
  q2 : Q

data P : Set where
  p1 : P
  p2 : P

data C : Set where
  c1 : C
  c2 : C

data D : Set where
  d1 : D
  d2 : D

-- Our little universe
data U : Set where
  d : U
  p : U

-- The interpretation function
⟦_⟧ : U → Set
⟦ d ⟧ = D
⟦ p ⟧ = P

f : U → Set
f d = Q
f p = C

-- An example of how to use f:
omo : {u : U} → ⟦ u ⟧ → f u
omo {d} d1 = q1
omo {d} d2 = q2
omo {p} p1 = c1
omo {p} p2 = c2