{- LTypes contains labels for integers, booleans 
    and products -}  
let LTypes = <lint,lbool,lproduct>; 


{- A. Closed Version: Counts the number of integers in an arbitrary data
    structure -}  
let count = fix count: [A:*|LTypes].A -> Int.
            {- abstract over type A which can be instantiated with
                type mentioning LTypes -} 
            \A:*|LTypes. 
              typecase A of {
                lbool => \x:Bool.0
                      {- annotations: the schema and the labelset of
                          the branch; not important -} 
                      : \A:*.A -> Int
                      | LTypes, 
                lint => \x:Int.1 
                     : \A:*.A -> Int
                     | LTypes, 
                lproduct => 
                {- the lproduct is *->*->*, therefore this kind
                    indicates that we have to abstract over two type 
                    variables of kind * first, in order to then 
                    instantiate \A:*.A->Int with (A1*A2) -} 
                            \A1:*|LTypes,
                             A2:*|LTypes. 
                             \x:A1*A2. 
                                (count [A1] x.fst) + (count [A2] x.snd)
                          : \A:*.A -> Int 
                          | LTypes
               }

{- An example call site -} 
in count [(Int*(Int*(Bool*Int)))] (2,(3,(true,3)));

{- B. Extensible version. -} 
let ecount = {- first abstract the label set of the extension -} 
             \Ls:LABS.
             {- take an extension that can analyze Ls -}
             \extension: Ls => \A:*.A -> Int | LTypes++Ls. 
               fix count: [A:*|LTypes++Ls].A -> Int. 
                {- abstract a type in LTypes++Ls -} 
                 \A:*|LTypes++Ls. 
                   {- if A weak-head reduces to sth in LTypes, 
                      do what you did in the closed case -} 
                   typecase A of { 
                      lbool => \x:Bool.0
                            : \A:*.A -> Int
                            | LTypes++Ls, 
                      lint => \x:Int.1 
                           : \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
                   {- and add the extension for the extra types of Ls -}
                   } ++ extension;

{- For example, here's the trivial extension -} 
ecount [<>] { :\A:*.A -> Int | LTypes } [Int*Bool] (3,true);


{- Now let's extend it to arbitrary records! -} 
let extension = 
  {- it has to be recursive! because for elements of the records, it
     must call the __extended__ ecount function -} 
  fix extension:<lrec>=>\A:*.A->Int | LTypes++<lrec>. 
  { lrec => 
     {- lrec : MAP -> *, so we need first abstract over a MAP -} 
     {- reminder: MAPS are first-class maps between labels 
        (yes, ordinary labels!!) and types -} 
      \M:MAP | LTypes++<lrec>.
         {- Perform a map analysis. There are four cases -} 
         mapcase [\M:MAP.(lrec [M])->Int] M of {
           {- empty -}
            \x:(lrec [map of { }]).0,
           {- singleton map. abstract over the label, 
              abstract over the type and do what you have to do
            -}
            \li:LAB(*).\B:*|LTypes++<lrec>. 
            \x:(lrec [map of {li:B}]).
                {- call the _extended_ with myself count! -}  
                ecount [<lrec>] extension [B] (x.li),
           {- union of two MAPS, abstract over M1 and M2 first -} 
            \M1:MAP|LTypes++<lrec>,M2:MAP|LTypes++<lrec>. 
            \x:(lrec [(M1++M2)]). 
                {- x!M1 _restricts the type of x to appear as 
                   lrec [M1] instead of lrec [M1++M2]. This is
                   obviously sound (it resembles width subtyping 
                   for records) -} 
                (ecount [<lrec>] extension [(lrec [M1])] (x!M1)) +
                (ecount [<lrec>] extension [(lrec [M2])] (x!M2))
         }
             : \A:*.A->Int
             | LTypes++<lrec>
};


{- So, here's a typical call site for this! -} 
ecount [<lrec>] extension [{lFirst:Int*Int, lSecond : {lThird:Int}}] 
                              {lFirst=(3,3),lSecond = {lThird=2  }};

{- An Extension for Variants!  -} 
let extension_b = 
  {- Just as before, it must be recursive -} 
  fix extension:<lvar>=>\A:*.A->Int | LTypes++<lvar>. 
  { lvar => 
     {- lvar is also MAP -> *, so we abstract over the map and do 
        a mapcase -} 
      \M:MAP | LTypes++<lvar>.
         mapcase [\M:MAP.(lvar [M])->Int] M of {
           {- empty -}
            \x:(lvar [map of { }]).0,
           {- singleton: we abstract over the label/type -}
            \li:LAB(*).\B:*|LTypes++<lvar>. 
            \x:(lvar [map of {li:B}]). 
                {- now we need to pattern match (!) to get what the
                   thing has inside. i don't have a good writeup for
                   pattern matching semantics and exhaustiveness 
                   search---check the implementation for this. 
                   
                   Roughly speaking we can pattern 
                   match against label variables only when we are
                   sure that it is sound, ie for example, there is no 
                   case that some other instantiation of some other 
                   label variable will cause the term to get
                   stuck. This is trivially true for singleton maps 
                   (variants) -} 
                (match x with 
                 li(e) -> (ecount [<lvar>] extension [B] (e))),
           {- union: as before we first abstract M1 and M2  -} 
            \M1:MAP|LTypes++<lvar>,M2:MAP|LTypes++<lvar>. 
            \x:(lvar [(M1++M2)]). 
                {- but now it is not sound to assume a "!" restrict
                   operator like the record case. instead we introduce 
                   a varcase, that depending on the type of the 
                   expression, it will bind it to a variable either 
                   of (lvar [M1] or (lvar [M2]). The semantics of 
                   this can only be found in the implementation 
                   unfortunately  -} 
                varcase x of 
                  y:(lvar [M1]) -> (ecount [<lvar>] extension [(lvar [M1])] y)
                | y:(lvar [M2]) -> (ecount [<lvar>] extension [(lvar [M2])] y)
         }
             : \A:*.A->Int
             | LTypes++<lvar>
  };

{- So, let's try it out ... -} 
let XType = {  
        lTypeOne of (Int*Int) 
      | lTypeTwo of Int };

{- Call site.-} 
ecount [<lvar>] extension_b [XType] (lTypeOne((3,2)):XType)