Re: [isabelle] type inference in HOL



Quoting Christian Urban <urbanc at in.tum.de>:

Florian Haftmann writes:
 >
 > The point is that you don't state anything about the type parameters 'b
 > and 'c of funA in funB_def since they do not occur on the left hand side
 > of funB_def; you have to instantiate them:
 >
 > defs
> funB_def : "funB == lftsnd (funA :: 'a => (unit => unit) * ('d => 'e))"

An alternative is to parametrise funB with the types not mentioned.
For example

  consts
    lftsnd :: "('a => 'b * 'c) => 'a => 'c"
    funA   :: "'a => ('b => 'c) * ('d => 'e)"

  defs
    lftsnd_def : "lftsnd f x == snd (f x)"

  constdefs
funB_def: "funB TYPE('b) TYPE('c) == lftsnd (funA::'a=>('b=>'c)*('d=>'e))"


If I parametrise the function, may I instantiate the type parameters later on, or do I have to bring them with me explicitly all along? anything in the documentation?

The reason why all type-variables of a right-hand side
of a definition have to occur on the left-hand side as
well is that otherwise one can write down definitions
that lead to inconsistencies.

Do you know if it is generally the case that unistantiated variables lead to
inconsistencies? I mean, take something like

consts
consA :: "('a*bool)"

constdefs
consB_def : "consB == snd consA"

I was just wondering how one may get an inconsistency from there.

Cheers,
Paolo









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.