Probably with a function with a type signature something like this (which is in Agda, another dependently typed language, but the idea holds):

    nGram : {l : Nat}{n : Fin l} -> Vec l Char -> n -> List (Vec n Char)

To break it up:

    "nGram" is the name of the function
    
    "{l : Nat}" means l is a natural number
    
    "{n : Fin l}" means n is a finite number smaller than l
    
    "Vec l Char" is the first argument, declared as a 
    vector of characters, with length l
    
    "n" is the second argument (previously declared as
    a finite number smaller than l)
    
    "List (Vec n Char)" is the return type, a list which consists 
    of vectors of characters where each vector is of length n

For an explanation on how and why this works you can check out these papers:

http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWo...

The first is more about programming in Agda while the second goes into how dependently typed languages relate to logic. Together they provide sufficient definitions of Nat, Fin, Vec and List to declare the nGram function.

If you're unfamiliar with ML-style syntax the above definiton probably looks weird, but can be written in a pseudo-java style like this:

   List<Vec<N,Char>> nGram<Nat L,Fin<L> N>(Vec<L,Char> input_string, N n){}