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

[wagnerdm@seas.upenn.edu]

Quoting "giacomo90 at libero.it" <giacomo90 at libero.it>:

> 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]));

That type annotation on hd looks suspicious. Perhaps you can make  
headway by changing it to "lambda hd:Varexpr A"? You might also try  
defining the "map" function that you may know from OCaml for applying  
a function to each element of a list.

> 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)
>               );

I guess I don't know exactly which fixpoint operator is available in  
the language you're using, but one common type for it looks like

fix : forall a. (a -> a) -> a

So, if the final function you want has type (Mynat -> Mynat -> Bool),  
then the  function you need to take a fixpoint of has type

((Mynat -> Mynat -> Bool) -> (Mynat -> Mynat -> Bool)).

Does that help? If not, then my intuition for writing fixpoints is  
that they should take a function that knows what to do for "small"  
input values, and write a new function that knows what to do for  
slightly larger input values -- e.g. for ones with one more "succ",  
or, in the case of your other question, for ones with one more "in".

Perhaps these suggestions can help you figure out the answers for yourself. =)
~d