{- A counter of useful elements in a data structure. Taken from 
   Ralf Hinze's  paper. -}

{- again consider a 'base' label set -} 
let LTypes = <lint,lbool,lproduct>; 

{- Extensible version of ecount where all constructors return 0 -} 
{- The name of the game is that we are going to rename a given type to
   sth else, and pass this function an extension that treats that new
   name in a special way. -} 
let ecount = \Ls:LABS.
             \extension: Ls => \A:*.A -> Int | LTypes++Ls. 
               fix count: [A:*|LTypes++Ls].A -> Int. 
                 \A:*|LTypes++Ls. 
                   typecase A of { 
                      lbool => \x:Bool.0
                            : \A:*.A -> Int
                            | LTypes++Ls, 
                      lint => \x:Int.0
                           : \A:*.A -> Int
                           | LTypes++Ls, 
                      lproduct => 
                          \A1:*|LTypes++Ls,
                           A2:*|LTypes++Ls. 
                            \x:A1*A2. 
                              (count [A1] x.fst) + (count [A2] x.snd)
                               : \A:*.A -> Int 
                               | LTypes++Ls
                   } ++ extension;

{- Suppose we want to check how many A's are in an element of 
the following structure. The answer should be  always 4, even when 
we instantiate A with Bool. The trick becomes interesting in the case
of recursive types, but for the sake of simplicity we present with an
ordinary type (the reason is, in the current implementation only generative
types can be recursive and using generative types would make the code
look awful and full of coercions ...) -} 
let Struct = 
        \A:*. ((A*A)*((A*Bool)*A));

{- To do this, we create a new function ecount2 -}
let ecount2 = 
        {- abstract over a constructor, like Struct, and the 
           abstract over the argument of that constructor -}  
	 \F:*->*|LTypes.
	    \A:*|LTypes. 
          {- now, take a function that knows how 
             to treat that A type -} 
          \f:(A -> Int).
                  {- generate a new name, isomorphic but not
                     equivalent to A, and take the argument x -}
	          new lA : * = A in
	           \x: F A. 
                     {- call ecount extending it for label lA 
                        by passing a special branch that essentially 
                        calls f after coercing the argument type to A
                        again -} 
	             ecount [<lA>] 
                            { lA => 
                                   \x:lA. 
                                     f (fromLabelPrim lA x: lA) 
                                 : \A:*.A->Int 
                                 | LTypes++<lA> } 
                            [F lA]
                            {- in order for this to work we have to
                               coerce the argument, from F A to F lA, 
                               otherwise one of the already
                               existing branches will be called and we 
                               are going to lose the
                               distinctions we wanted to impose (namely, 
                              to call f instead of falling in one of the 
                              other branches)  -} 
	                    (toLabelExt lA x : F A);

{- Here we go ... Just return 1 when you encouter a useful data -} 
ecount2 [Struct][Int] (\x:Int. 1) ((1,2),((3,true),4))