Re: [isabelle] type inference in HOL

Quoting Christian Urban <urbanc at>:

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

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

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

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

consA :: "('a*bool)"

consB_def : "consB == snd consA"

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


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