**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.

###### Asked By : user2435797

#### 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).

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/54709

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback