Utilizziamo la notazione di Haskell per denotare il tipo
"lista di elementi di tipo T": [T]
Introduciamo poi le costanti "cons", "hd" e "tail".
Ovviamente gli assiomi e le regole valgono per ogni possibile T. 


      B |- L : [T]     B |- M : T
 -----------------------------------
            B |- cons M L : [T]



      -------------------------------
           B |- emptylist : [T]

 

         B |- L : [T]    L diverso da emptylist
    -------------------------------------------
         B |- hd L : T



      B |- L : [T]        L diverso da emptyist
  -----------------------------------------------
      B |- tail L : [T]


Ovviamente possiamo anche utilizzare, al posto delle regole di inferenza
sopra descritte, gli assiomi seguenti:


   -----------------------------------------------
            B |- cons : T -> [T] -> [T]



      -------------------------------
           B |- emptylist : [T]


      --------------------------------
            B |- hd : [T] -> T 


 ----------------------------
    B |- tail L : [T] -> [T]

con questo approccio si capisce pero' che il sistema
permette di tipare cose come hd emptylist oppure tail emptylist.