Demonstration of how we can "fake" a dependently typed list in Ceylon.

vectors.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>()
        satisfies Summable<Vec<N>>
        given N satisfies Nat {
   
   shared formal String elementsString;
   
   string => "[``elementsString``]";
   
}

"A vector of length zero."
abstract class Nil() of nil 
        extends Vec<Zero>() {
   
   shared actual Nil plus(Vec<Zero> that)
           => this;
   
   elementsString => "";
   
}

"The singleton instance of `Nil`."
object nil extends Nil() {}

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


void testDepTypeVectors() {
    value v = Cons(1.0, Cons(2.0, Cons(-1.0, nil)));
    value u = Cons(3.0, Cons(2.0, nil));
    value w = Cons(-1.0, u);
    print(v + w);
}