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 ?
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