Expressing normal data types such as lists and nats is straightforward and there are many examples around. What is the generic procedure to translate GADTs, though? Some examples translating typical types such as Vector and dependent products from Idris to Morte would be very illustrative.
You can't get eliminators that depend on elements of data types, but you can define eliminators that depend on indices of elements of data types. Hence, Vectors are representable (the code is in Agda):
Nat = (P : Set) -> (P -> P) -> P -> P
zero : Nat
zero = λ P f z -> z
suc : Nat -> Nat
suc = λ n P f z -> f (n P f z)
plus : Nat -> Nat -> Nat
plus = λ n m P f z -> n P f (m P f z)
Vec = λ (A : Set) (n : Nat) ->
(P : Nat -> Set) -> (∀ n -> A -> P n -> P (suc n)) -> P zero -> P n
nil : ∀ A -> Vec A zero
nil = λ A P f z -> z
cons : ∀ A n -> A -> Vec A n -> Vec A (suc n)
cons = λ A n x xs P f z -> f n x (xs P f z)
concat : ∀ A n m -> Vec A n -> Vec A m -> Vec A (plus n m)
concat = λ A n m xs ys P f z -> xs (λ n -> P (plus n m)) (λ n -> f (plus n m)) (ys P f z)
These are very similar to Church-encoded lists, you just make a type, that you eliminate into, dependent on the indices of a data type being defined and change induction hypotheses to reflect the structure of the constructors of the data type. I.e. you have
cons : ∀ A n -> A -> Vec A n -> Vec A (suc n)
so the corresponding induction hypothesis is
∀ n -> A -> P n -> P (suc n)
In order to define dependent pairs without inductive types, you need very/insanely dependent types (sigmas are here), which allow the result of a function depend on this same function being defined. Morte doesn't have this, of course.