Email Gateway (Aug 19 2022 at 14:34): Email Gateway (Aug 19 2022 at 14:34):From: Lars Hupel <hupel@in.tum.de>
This works exactly as expected. Thanks!
Lars
Email Gateway (Aug 19 2022 at 14:47):From: Lars Hupel <hupel@in.tum.de>
Hello,
I'm trying to produce well-sorted terms in Isabelle/ML. Basically, I
have a predicate "P" of type "'a" with some sort constraint, and I want
to apply it to some polymorphic constant. Consider this small Isar
snippet:
class foo
consts
P :: "'a::foo ⇒ bool"
opt :: "'a option"
instantiation option :: (foo) foo
begin
instance ..
end
declare [[show_sorts]]
ML_val{* @{term "P opt"} *}
As is obvious from the output, type inference instantiates P's type to
'a∷foo option ⇒ bool
The important bit here is that it slapped a "foo" constraint on the
type variable.
However, it is not obvious to me how to do the same thing in ML. I
mean, it's trivial to construct a well-typed term for "P opt":
ML{*
fun mk_P t = Const (@{const_name P}, fastype_of t --> @{typ bool}) $
t;
val t = mk_P @{term opt};
val ct = cterm_of @{theory} t;
*}
... but the sort constraint is missing on the instantiated type of "P".
A very "hackish" approximation for this problem is to go through
"fastype_of t" and replace all sort constraints by "[foo]", because I
can (sort of) assume that all my instantiations for "foo" only require
"foo" for the type variables. I feel that there ought to be a better
solution, though.
Why do I even need well-sorted terms? I have rules which look like
this:
P x ⟹ P (Some x)
and I cannot apply them unless the sorts line up.
(In my formalization, the type constructor is not "option", but "fun",
but the idea is the same.)
Cheers
Lars
Email Gateway (Aug 19 2022 at 14:48):From: Dmitriy Traytel <traytel@in.tum.de>
Sounds to me like you just would want to use the type inference itself:
ML{*
fun mk_P t = Const (@{const_name P}, dummyT) $ t |> Syntax.check_term
@{context};
val t = mk_P (Const (@{const_name opt}, dummyT));
val ct = cterm_of @{theory} t;
*}
You can refine the "dummyT"s if the type that you get is too general.
Hope that helps,
Dmitriy
Last updated: Apr 26 2024 at 08:19 UTC