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:
> funB_def : "funB == lftsnd (funA :: 'a => (unit => unit) *
('d => 'e))"
An alternative is to parametrise funB with the types not mentioned.
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
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