The generalization is to allow constructors of any arity.
type
g
(
τ
) =
C
g
of
τ
i
∣ …
C
g
of
τ
n
This is rather easy and left as an exercise. Then, one could define:
type
(α
1
, α
2
) (_ * _) = (_, _) of (α
1
, α
2
)
fst =
def
λ
z
. (
F
*
z
(λ
x
. λ
y
.
x
))
snd =
def
λ
z
. (
F
*
z
(λ
x
. λ
y
.
y
))