Generalization of Vec over element types.

genericVectors.ceylon

"Encoding of natural numbers at 
 type level."
interface Nat of Zero|Succ<Nat> {}
"The natural number `0`."
interface Zero satisfies Nat {}
"The natural number `N+1` for a
 given natural number `N`."
interface Succ<N>
        satisfies Nat
        given N satisfies Nat {}
 
"A vector of length `N`."
abstract class Vec<N,T>()
        satisfies Summable<Vec<N,T>>
        given N satisfies Nat {
   
   shared formal String elementsString;
   
   string => "[``elementsString``]";
   
}
 
"A vector of length zero."
class Nil<T>() 
        extends Vec<Zero,T>() {
   
   shared actual Nil<T> plus(Vec<Zero,T> that)
           => this;
   
   elementsString => "";
   
}

"A vector of length `N+1`, for a 
 given element and given vector of 
 length `N`."
class Cons<N,T>(head, tail) 
        extends Vec<Succ<N>,T>() 
        given N satisfies Nat {
    
    shared Float head;
    shared Vec<N,T> tail;
    
    shared actual Cons<N,T> plus(Vec<Succ<N>,T> that) {
        assert (is Cons<N,T> that);
        return Cons<N,T>(this.head + that.head, 
                this.tail.plus(that.tail));
    }
    
    elementsString => tail is Nil<T>
            then head.string 
            else head.string + ", " + tail.elementsString;
    
}