World's most popular travel blog for travel bloggers.

# [Answers] How to write a closed term with this type?

, ,
Problem Detail:

X→Y →(X+Y)×Y

I'm confused about how to get the type (X + Y). If I assume m: (X + Y), n: X, k: Y then I can get $${m:X+Y \vdash \lambda n:X.\lambda k:Y.<m, k>}$$ which get the right type. But I can't reduce the context m: X + Y. So, could anyone tell me how to make it? Thanks a lot.

#### Answered By : Andrej Bauer

Whenever a new type constructor is defined, it comes with introduction and elimination terms. These are part of the definition.

In the case of sums, the following are part of the definition of what it means to have $X + Y$:

• given types $X$ and $Y$ there is a type $X + Y$
• given a term $e : X$ there is a term $\mathsf{inl}(e) : X + Y$
• given a term $e' : Y$ there is a term $\mathsf{inr}(e') : X + Y$
• (there is also an eliminator and equations which I am not writing down here)

So I think this is the point you missed: we do not just say "there is a type $X + Y$" without anything else, as that would be completely useless. We also provide ways of constructing (introducing) and deconstructing (eliminating) terms of the new type.

Now that we know that $\mathsf{inl}$ and $\mathsf{inr}$ are there by definition of sum types, it is easy: $$\lambda x : X . \lambda y : Y . \langle \mathsf{inr}(y), y\rangle.$$ By the way, Haskell's djinn package can help you with this (I'd show a demo but OSX El Capitan broke cabal).