Idris Examples
Vectors
In both the dependent sum type and the dependent product type examples below the type declaration has two terms where the second depends on the first. However the definition of the sum type requires a specific value wheras the definition of the product type applies to all possible values.
Dependent Sum Type (dependent pair) 
myvect : (n:Nat ** Vect n String) myvect = (3 ** ("a", "b", "c") 
Dependent Product Type  myvect : n:Nat > (Vect n String) myvect n = 3 *n 
Implemetations of Dependent Product Type
Vect is an example of a type which depends on:

 Vectors: Generic lists with explicit length in the type  @ len the length of the list  @ elem the type of elements data Vect : (len : Nat) > (elem : Type) > Type where  Empty vector Nil : Vect Z elem  A nonempty vector of length `S len`, consisting of  a head element and the rest of the list, of length `len`. (::) : (x : elem) > (xs : Vect len elem) > Vect (S len) elem 
So in this example we are saying that Vect exists for all types 'elem' and for all numbers 'len'.
Most programs that support this have a special notation for it.
So this is a product type where one of the types is a function (family of types).
So instead of the usual product:  Pair A B  
we have :  DPair A (A > Type)  
For example:  DPair Nat (Nat > Type)  
There is a special notation in Idris:  A ** (A > Type) 
Notation
~> idris p base Data/Vect.idr / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 1.3.2 _/ // /_/ / / / (__ ) http://www.idrislang.org/ /___/\__,_/_/ /_/____/ Type :? for help Idris is free software with ABSOLUTELY NO WARRANTY. For details type :warranty. *Data/Vect> (n : Nat ** Vect n String) (n : Nat ** Vect n String) : Type 
Example
In the introduction dependent types were introduced with the example of vect. 
specificVect : (n : Nat ** Vect n String) specificVect = (3 ** ["a","b","c"]) 
We can also show dependent sum types using Vect.  *typeTheory> specificVect (3 ** ["a", "b", "c"]) : (n : Nat ** Vect n String) 
In the product case there was a type for every n which is represented by a function (n > Vect n elem). In the sum case there is one type given by a single 'n' which is represented by a product/tuple (n ** Vect n elem) but because the second element of the tuple depends on the first '**' is used to seperate the elements instead of ','.
Example  Expressions
The aim here is to try to model the context of variable declarations (or of premises in logic) as an index.
Start by creating a very simple expression type to work with.   Expression over some type 't' data Expression t = Lit t Var String (+) (Expression t) (Expression t) 
Now give it the ability to bind   Expression which binds some variable 'v' data BindExpression t (v:String) = BoundVar v (Expression t) Nested v (BindExpression t v) 
I haven't yet worked this through.
Example  Variable Scope
Here we try to model the situation where we define variables and then use them either in the same block or in a sub block. So we need to determine which definition to use based on the scope.
How can we revers the arrows so that we can get back to a definition from a variable use?
Implementation Code
Idrisfrom : Idrisdev/libs/prelude/Builtins.idr 
 Dependent pairs aid in the construction of dependent types by  providing evidence that some value resides in the type.   Formally, speaking, dependent pairs represent existential  quantification  they consist of a witness for the existential  claim and a proof that the property holds for it.   @a the value to place in the type.  @P the dependent type that requires the value. data DPair : (a : Type) > (P : a > Type) > Type where MkDPair : .{P : a > Type} > (x : a) > (pf : P x) > DPair a P 
Dependent Types in Programming
In the language 'Scala' we can define a type that is parameterised by another type (polymorphism) for instance:  List[T] 
This represents a list of any type, represented by 'T', for example a list of Integers or a list of boolean values.
However, Scala does not allow dependent products like say: Modulo[n:Integer] which would represent any modulo number system such as modulo 3 or modulo 27.