[TYPES] Not able to define some recursive types in "Fullfomsubref"

[giacomo90@libero.it]

Hello,
          I am a CS student at Bologna University and I'm studiying Pierce's 
book on my own.
          The first problem concerns the definition of inductive types with 
variants. I want to define a datatype that in OCaml should be:

# type 'a varexpr = EVal of 'a | EVar of string | EList of ('a varexpr lis)


          So it would be typed as:

# Varexpr = lambda A. All X. (A->X)->(String->X)->(List X->X)->X;


          I have no problems defining the costructor for the EVal or EVar 
case, but my problem is defining the EList case:

# elis = lambda A. lambda arg:List (Varexpr A). 
          (lambda X. lambda l:(A->X). lambda r:(String->X). lambda t:(List X-
>X). (t ...... )
          )


          but it's not correct if I write (t arg)  because I don't pass to arg 
the arguments "[X] l r t". And even the following form is not correct:

# ell = lambda A. lambda arg:List (Varexpr A). 
      lambda X. lambda l:(A->X). lambda r:(String->X). lambda t:(List X->X).
        t (arg [List X] (lambda hd:X. lambda tl:List X. cons [X] (hd [H] l r 
t) tl ) (nil [X]));


          Another problem that I have is the definition of a double-recursive 
algorithm, such as defining the equivalence of two values (ie.) of the same 
type. For example an algorithm in OCaml for defining equivalence recursively 
is:

# let rec eqnat x y = 
    match x with
        | O -> ( match y with O -> true | _ -> false)
        | S t -> (match y with O -> false | S u -> eqnat t u)


          But I cannot find a solution without using the letrec construct wich 
uses the fix operator; in fact the following form is not correct:

# /* using the constructors o and s(x) similarly in OCaml */
# eqnat = lambda x:Mynat. lambda y:Mynat. 
               ( x [Bool] (lambda x1:Bool. (y [Bool] (lambda y1:Bool.  ...x...
y...? ) false ))
                                (y [Bool] (lambda y1:Bool. false) true)
              );


          Even if i could use an algorithm with one way recursion as:

# and = lambda a:Boolean. lambda b:Boolean. (a [Boolean] b f);
# isZer = lambda u:Natu. (u [Boolean] (lambda x:Boolean. f) t);
# sub = lambda a:Natu. lambda b:Natu. (b [Natu] (lambda x:Natu. precN x) a);
# eqN = lambda a:Natu. lambda b:Natu. and (isZer (sub a b)) (isZer (sub b a));


          Another problem related to the first one is the definition of a 
simple recursive datatype that I could define in OCaml as follows:

# type 'a rec = In ('a rec -> 'a)
# let out (In x) = x


          And I think that is of a type

# Recu = lambda A. All X. ((X->A)->X)->X;


          But, I think, for the same problem, I cannot definre the costructor 
"In" for the datatype Recu. All this in order to define the Y operator like I 
could do in OCaml:

# let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))


         I would really appreciate any answer to my questions or even a 
suggestion. Is my aim vain to pursue? 
         Thanks. Regards.


Giacomo Bergami.