On Tue, Dec 10, 2013 at 11:43 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

>
> As always, Gabriel's answer is correct, but I have two remarks.
> First, concerning your first example where you needed annotations on the
> local function,
> you can actually avoid that by using pattern matching rather than function
> application:
>
> I realized that after posting :-)


>
> Now, for the above example, of course you don't need to annotate the
> "function" construct,
> but if you want to name the rigid variables 't47 and 't59, you can do that
> through eta-expansion:
>
> let rec eval : type a . (a term -> a) =
>   function Lit i -> i | IsZero x -> is_zero (eval x)
>     | Plus (x, y) -> plus (eval x) (eval y)
>     | If (b, t, e) -> if_then (eval b) (eval t) (eval e)
>     | Pair (x, y) -> (eval x, eval y)
>     | Fst p -> (fun (type b) p -> let ((x, y): (a * b)) = eval p in x) p
>     | Snd p -> (fun (type b) p -> let ((x, y): (b * a)) = eval p in y) p
>
> Not very clean, so we need to do something about it.
>
> I do not need it, I am just exploring ways of outputting that information
in case someone would find it useful (under the big conditional that
someone would find InvarGenT useful in the first place, rather than just
cool...)