Solving the Problem

First we need the type of our function split:

split: list alpha -> list alpha # list alpha;

What does split do?

split(k) <= (firstHalf k,secondHalf k);

This will work fine provided that we have functions firstHalf and functions secondHalf with the following specification:

Specification: firstHalf is a function which takes a list k and returns a list consisting of the first length(k) div 2 elements of the list. For example firstHalf [1,2,3,4,5] should give [1,2] since the length is 5 and 5 div 2 is 2.

Now what about secondHalf? secondHalf is a function which takes a list k and returns a list consisting of k after the first length(k) div 2 elements k have been thrown away. So we have

firstHalf: list(alpha) -> list(alpha);
firstHalf k <= keep( (length k) div 2 ,k);

secondHalf: list(alpha) -> list(alpha);
secondHalf k <= throwAway( (length k) div 2 ,k);

So all that is left to do is specify and design keep and throwAway.

The function keep takes a number n and a list k and returns a list consisting of the first n elements of k. That's easy:

keep: num # list(alpha) -> list(alpha);
keep(0,k) <= [];
keep (n+1,x::k) <= x::keep(n,k);

The function throwAway takes a number n and a list k and returns list k with the first n elements thrown away.

throwAway: num # list(alpha) -> list(alpha);
throwAway(0,k) <= k;
throwAway (n+1,x::k) <= throwAway(n,k);

Our task is now complete. This gives is the complete Hope program:

throwAway: num # list(alpha) -> list(alpha);
throwAway(0,k) <= k;
throwAway (n+1,x::k) <= throwAway(n,k);

keep: num # list(alpha) -> list(alpha);
keep(0,k) <= [];
keep (n+1,x::k) <= x::keep(n,k);

length: list(alpha) -> num;
length [] <= 0;
length (x::k) <= 1 + length k;

firstHalf: list(alpha) -> list(alpha);
firstHalf k <= keep( (length k) div 2 ,k);

secondHalf: list(alpha) -> list(alpha);
secondHalf k <= throwAway( (length k) div 2 ,k);

split: list alpha -> list alpha # list alpha;
split(k) <= (firstHalf k,secondHalf k);